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