Lemma isbinopfuntoabgrdiff (X : abmonoid) : isbinopfun (toabgrdiff X). Proof. unfold isbinopfun. intros x1 x2. change (setquotpr _ (x1 + x2 ,, 0) = setquotpr (eqrelabgrdiff X) (x1 + x2 ,, 0 + 0)). apply (maponpaths (setquotpr _)). apply (@pathsdirprod X X). - apply idpath. - exact (!lunax X 0). Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.