Definition nat_nat_prod_abmonoid_monoidfun {X : abgr} (x : X) : monoidfun (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) X. Proof. use monoidfunconstr. - exact (nataddabmonoid_nataddabmonoid_to_monoid_fun x). - use make_ismonoidfun. + exact (nat_nat_monoid_fun_isbinopfun x). + exact (nat_nat_prod_abmonoid_fun_unel x). Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.