Lemma nat_nat_monoid_fun_isbinopfun {X : abgr} (x : X) : isbinopfun (nataddabmonoid_nataddabmonoid_to_monoid_fun x). Proof. use make_isbinopfun. intros n m. induction n as [n1 n2]. induction m as [m1 m2]. cbn. unfold nataddabmonoid_nataddabmonoid_to_monoid_fun. unfold nat_nat_to_monoid_fun. cbn. rewrite nat_to_abmonoid_fun_plus. rewrite nat_to_abmonoid_fun_plus. rewrite (assocax X). rewrite (assocax X). use two_arg_paths. - use idpath. - rewrite <- (assocax X). rewrite (commax X (nat_to_monoid_fun (grinv X x) n2) _). rewrite (assocax X). rewrite (assocax X). use two_arg_paths. + use idpath. + use (commax X). Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.