proposition: Lemma natmult_op {X : monoid} : ∏ (n : nat) (x y : X), (x + y = y + x)%addmonoid -> natmult n (x + y)%addmonoid = (natmult n x + natmult n y)%addmonoid.
proof: Proof. intros. induction n as [|n IHn]. - rewrite lunax. reflexivity. - rewrite natmultS, assocax, IHn, <- (assocax _ y). assert (X1 : (y + natmult n x = natmult n x + y)%addmonoid). { clear IHn. induction n as [|n IHn]. - rewrite lunax, runax. reflexivity. - rewrite !natmultS, <- assocax, <- X0, !assocax, IHn. reflexivity. } rewrite X1, assocax, <- natmultS, <- assocax, <- natmultS. 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