fact: Definition nattorig {X : rig} (n : nat) : X := natmult (X := rigaddabmonoid X) n 1%rig.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics