proposition: Lemma isarchhz : isarchring (X := hz) hzgth.
proof: Proof. simple refine (isarchrigtoring _ _ _ _ _ _). - reflexivity. - intros n m. apply istransnatgth. - apply isarchrig_setquot_aux. + split. * apply natgthandpluslinv. * apply natgthandplusrinv. + apply isarchnat. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra