proposition: 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: Proof. intros. apply isinclbetweensets. apply (setproperty X). apply (setproperty (commringfrac X S)). intros x x'. intro e. set (e' := invweq (weqpathsinsetquot (eqrelcommringfrac X S) (make_dirprod x a') (make_dirprod x' a')) e). set (e'' := weqhrelhrel0commringfrac X S iscanc (make_dirprod _ _) (make_dirprod _ _) e'). simpl in e''. apply (invmaponpathsincl _ (iscanc a')). apply e''. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids