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