Lemma hz_abmonoid_ismonoidfun : @ismonoidfun (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) hzaddabgr (@setquotpr (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) (binopeqrelabgrdiff (rigaddabmonoid natcommrig))). Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use idpath. - use idpath. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.