Definition ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig : ConstructiveCommutativeDivisionRig → ConstructiveDivisionRig := λ X, (pr1 (pr1 X),,pr1 (pr2 (pr1 X))) ,, (pr2 X).
Require Import UniMath.MoreFoundations.Tactics.