proposition: Lemma isarchgr_isarchmonoid {X : abgr} (R : hrel X) : isbinophrel R -> isarchgr R -> isarchmonoid (X := abgrtoabmonoid X) R.
proof: Proof. intros Hop H x y1 y2 Hy. split. - now apply H. - generalize (H (grinv X x) _ _ Hy). apply hinhfun. intros (n,Hn). exists n. apply isarchgr_isarchmonoid_aux. exact Hop. exact Hn. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics