Definition ConstructiveField_ConstructiveCommutativeDivisionRig : ConstructiveField → ConstructiveCommutativeDivisionRig := λ X, (commringtocommrig (pr1 X)) ,, (pr2 X).
Require Import UniMath.MoreFoundations.Tactics.