proposition: Lemma natmultS : ∏ {X : monoid} (n : nat) (x : X), natmult (S n) x = (x + natmult n x)%addmonoid.
proof: Proof. intros X n x. induction n as [|n]. - now rewrite runax. - reflexivity. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics