Lemma nattorigS {X : rig} : ∏ (n : nat), nattorig (X := X) (S n) = (1 + nattorig n)%rig. Proof. intros. now apply (natmultS (X := rigaddabmonoid X)). Qed.
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.