Definition ConstructiveDivisionRig_apsetwith2binop : ConstructiveDivisionRig → apsetwith2binop. Proof. intros X. exists (pr1 (pr1 (pr1 X)),,(pr1 (pr2 X))). split. exact (_,,(pr1 (pr2 (pr2 X)))). exact (_,,(pr1 (pr2 (pr2 (pr2 X))))). Defined.
Require Import UniMath.MoreFoundations.Tactics.