Lemma natmult_plus : ∏ {X : monoid} (n m : nat) (x : X), natmult (n + m) x = (natmult n x + natmult m x)%addmonoid. Proof. induction n as [|n IHn] ; intros m x. - rewrite lunax. reflexivity. - change (S n + m)%nat with (S (n + m))%nat. rewrite !natmultS, IHn, assocax. 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.