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. 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.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.