proposition: Lemma isarchmonoid_isarchgr {X : abgr} (R : hrel X) : isarchmonoid (X := abgrtoabmonoid X) R -> isarchgr R.
proof: Proof. intros H x y1 y2 Hy. apply (isarchmonoid_1 _ H x y1 y2 Hy). 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