Lemma ispartbinopcommringfracgt (X : commring) (S : @submonoid (ringmultabmonoid X)) {R : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) R) (is1 : isringmultgt X R) (is2 : ∏ c : X, S c → R c 0) : @ispartbinophrel (ringmultabmonoid X) S R. Proof. intros. split. - intros a b c s rab. apply (isringmultgttoislringmultgt X is0 is1 _ _ _ (is2 c s) rab). - intros a b c s rab. apply (isringmultgttoisrringmultgt X is0 is1 _ _ _ (is2 c s) rab). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.