Lemma isarchgr_isarchmonoid {X : abgr} (R : hrel X) : isbinophrel R → isarchgr R → isarchmonoid (X := abgrtoabmonoid X) R. 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.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.ConstructiveStructures. Require Import UniMath.MoreFoundations.Tactics.