Lemma isarchhz : isarchring (X := hz) hzgth. Proof. simple refine (isarchrigtoring _ _ _ _ _ _). - reflexivity. - intros n m. apply istransnatgth. - apply isarchrig_setquot_aux. + split. * apply natgthandpluslinv. * apply natgthandplusrinv. + apply isarchnat. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.