proposition: 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: 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.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids