Lemma nat_nat_prod_abmonoid_fun_unel {X : abgr} (x : X) : (nataddabmonoid_nataddabmonoid_to_monoid_fun x) (unel (abmonoiddirprod nataddabmonoid nataddabmonoid)) = (unel X). Proof. use (pathscomp0 (lunax X _)). use idpath. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.