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. 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.
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.