proposition: Lemma nat_to_monoid_fun_S {X : abmonoid} (x : X) (n : nat) : nat_to_monoid_fun x (S n) = (nat_to_monoid_fun x n * x)%multmonoid.
proof: Proof. induction n as [ | n IHn]. - exact (commax X x (unel X)). - cbn. rewrite (assocax X). use two_arg_paths. + use idpath. + exact (commax X x _). Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra