Definition isdeccommringfracgt (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) (is' : @ispartinvbinophrel (ringmultabmonoid X) S R) (isd : isdecrel R) : isdecrel (commringfracgt X S is0 is1 is2). Proof. intros. apply (isdecabmonoidfracrel (ringmultabmonoid X) S (ispartbinopcommringfracgt X S is0 is1 is2) is' isd). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.