proposition: Lemma isbinopfuntoabgrdiff (X : abmonoid) : isbinopfun (toabgrdiff X).
proof: Proof. unfold isbinopfun. intros x1 x2. change (paths (setquotpr _ (make_dirprod (x1 + x2) (unel X))) (setquotpr (eqrelabgrdiff X) (make_dirprod (x1 + x2) ((unel X) + (unel X))))). apply (maponpaths (setquotpr _)). apply (@pathsdirprod X X). apply idpath. apply (pathsinv0 (lunax X 0)). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids