Lemma isinclprabmonoidfrac (X : abmonoid) (A : submonoid X) (iscanc : ∏ a : A, isrcancelable (@op X) (pr1carrier _ a)) : ∏ a' : A, isincl (λ x, prabmonoidfrac X A x a'). Proof. intro a'. apply isinclbetweensets. - apply (setproperty X). - apply (setproperty (abmonoidfrac X A)). - intros x x'. intro e. set (e' := invweq (weqpathsinsetquot (eqrelabmonoidfrac X A) (x ,, a') (x' ,, a')) e). set (e'' := weqhrelhrel0abmonoidfrac X A iscanc (_ ,, _) (_ ,, _) e'). simpl in e''. apply (invmaponpathsincl _ (iscanc a')). apply e''. Defined.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.