Definition isdecfldfracgt (X : intdom) (is : isdeceq X) {R : hrel X} (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (is2 : R 1 0) (nc : neqchoice R) (isa : isasymm R) (isr : isdecrel R) : isdecrel (fldfracgt X is is0 is1 is2 nc). Proof. intros. unfold fldfracgt. intros a b. apply isdecabmonoidfracrel. - apply (pr1 (isinvringmultgtaspartinvbinophrel X R is0)). apply isinvringmultgtif. + apply is0. + apply is1. + apply nc. + apply isa. - apply isr. Defined.
Require Import UniMath.Algebra.Groups.