proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra