Lemma nattorig_natmult : ∏ {X : rig} (n : nat) (x : X), (nattorig n * x)%rig = natmult (X := rigaddabmonoid X) n x. Proof. intros. induction n as [|n IHn]. - now apply rigmult0x. - rewrite nattorigS, natmultS. now rewrite rigrdistr, IHn, riglunax2. 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.