Lemma isinclprcommringfrac (X : commring) (S : @submonoid (ringmultabmonoid X)) (iscanc : ∏ a : S, isrcancelable (@op2 X) (pr1carrier _ a)) : ∏ a' : S, isincl (λ x, prcommringfrac X S x a'). Proof. intros. apply isinclbetweensets. apply (setproperty X). apply (setproperty (commringfrac X S)). intros x x'. intro e. set (e' := invweq (weqpathsinsetquot (eqrelcommringfrac X S) (x ,, a') (x' ,, a')) e). set (e'' := weqhrelhrel0commringfrac X S iscanc (_ ,, _) (_ ,, _) e'). simpl in e''. apply (invmaponpathsincl _ (iscanc a')). apply e''. Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.