Lemma iscomptocommringfrac (X : commring) (S : @submonoid (ringmultabmonoid X)) {L : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) L) (is1 : isringmultgt X L) (is2 : ∏ c : X, S c → L c 0) : iscomprelrelfun L (commringfracgt X S is0 is1 is2) (tocommringfrac X S). Proof. apply (iscomptoabmonoidfrac (ringmultabmonoid X)). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.