Definition fldtointdom (X : fld) : intdom. Proof. exists (pr1 X). exists (pr1 (pr2 X)). intros a1 a2. induction (pr2 (pr2 X) a1) as [ a1' | e0 ]. - intro e12. rewrite <- (ringmultx0 (pr1 X) a1) in e12. set (e2 := lcanfromlinv _ _ _ _ (invtolinv _ _ a1') e12). apply (hinhpr (ii2 e2)). - intro e12. apply (hinhpr (ii1 e0)). Defined.
Require Import UniMath.Algebra.Groups.