Lemma isinclprabgrdiff (X : abmonoid) (iscanc : ∏ x : X, isrcancelable (@op X) x) : ∏ x' : X, isincl (λ x, prabgrdiff X x x'). Proof. intros. set (int := isinclprabmonoidfrac X (totalsubmonoid X) (λ a : totalsubmonoid X, iscanc (pr1 a)) (make_carrier (λ x : X, htrue) x' tt)). set (int1 := isinclcomp (make_incl _ int) (weqtoincl (invweq (weqabgrdiff X)))). apply int1. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.