proposition: Lemma isarchnat : isarchrig (X := natcommrig) natgth.
proof: Proof. repeat split. - intros y1 y2 Hy. generalize (isarchnat_diff y1 y2 Hy). apply hinhfun. intros n. exists (pr1 n). rewrite nattorig_nat. exact (pr2 n). - intros n. generalize (isarchnat_gth n). apply hinhfun. intros n'. exists (pr1 n'). rewrite nattorig_nat. exact (pr2 n'). - intros n. generalize (isarchnat_pos n). apply hinhfun. intros n'. exists (pr1 n'). rewrite nattorig_nat. exact (pr2 n'). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations