proposition: Lemma isinclprabgrdiff (X : abmonoid) (iscanc : ∏ x : X, isrcancelable (@op X) x) : ∏ x' : X, isincl (λ x, prabgrdiff X x x').
proof: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids