proposition: Lemma nattorig_nat : ∏ n : nat, nattorig (X := natcommrig) n = n.
proof: Proof. induction n as [|n IHn]. reflexivity. rewrite nattorigS, IHn. reflexivity. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations