Lemma natmult_mult : ∏ {X : monoid} (n m : nat) (x : X), natmult (n * m) x = (natmult n (natmult m x))%addmonoid. Proof. induction n as [|n IHn] ; intros m x. - reflexivity. - simpl (_ * _)%nat. assert (H : S n = (n + 1)%nat). { rewrite <- plus_n_Sm, natplusr0. reflexivity. } rewrite H ; clear H. rewrite !natmult_plus, IHn. 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.