Lemma nat_to_abmonoid_fun_plus {X : monoid} (x : X) (n m : nat) : nat_to_monoid_fun x (n + m)%nat = @op X (nat_to_monoid_fun x n) (nat_to_monoid_fun x m). Proof. revert m. induction n as [ | n IHn]. - intros m. rewrite (lunax X). use idpath. - intros m. cbn. rewrite (assocax X). use two_arg_paths. + use idpath. + exact (IHn m). Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.