proposition: Lemma nat_nat_monoid_fun_isbinopfun {X : abgr} (x : X) : isbinopfun (nataddabmonoid_nataddabmonoid_to_monoid_fun x).
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra