Definition isincltocommringfrac (X : commring) (S : @submonoid (ringmultabmonoid X)) (iscanc : ∏ a : S, isrcancelable (@op2 X) (pr1carrier _ a)) : isincl (tocommringfrac X S) := isinclprcommringfrac X S iscanc (unel S).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.