Lemma natmultS : ∏ {X : monoid} (n : nat) (x : X), natmult (S n) x = (x + natmult n x)%addmonoid. Proof. intros X n x. induction n as [|n]. - now rewrite runax. - 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.