proposition: Lemma iscomptoabgrdiff (X : abmonoid) {L : hrel X} (is : isbinophrel L) : iscomprelrelfun L (abgrdiffrel X is) (toabgrdiff X).
proof: Proof. unfold iscomprelrelfun. intros x x' l. change (abgrdiffrelint X L (make_dirprod x (unel X)) (make_dirprod x' (unel X))). simpl. apply (hinhpr). split with (unel X). apply ((pr2 is) _ _ 0). apply ((pr2 is) _ _ 0). apply l. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids