proposition: Lemma invertibilityincommringfrac (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : ∏ a a' : S, isinvertible (@op2 (commringfrac X S)) (prcommringfrac X S (pr1 a) a').
proof: Proof. intros. apply (invertibilityinabmonoidfrac (ringmultabmonoid X) S). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids