proposition: Lemma hz_abmonoid_ismonoidfun : @ismonoidfun (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) hzaddabgr (@setquotpr (abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig)) (binopeqrelabgrdiff (rigaddabmonoid natcommrig))).
proof: Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. use idpath. - use idpath. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra