Definition weqfldfracgtint_f (X : intdom) {R : hrel X} (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (is2 : R 1 0) (nc : neqchoice R) (xa : X × intdomnonzerosubmonoid X) : X × ringpossubmonoid X is1 is2. Proof. intros. induction (nc (pr1 (pr2 xa)) 0 (pr2 (pr2 xa))) as [ g | l ]. - apply (pr1 xa ,, pr1 (pr2 xa) ,, g). - exists (- (pr1 xa)). exists (- (pr1 (pr2 xa))). simpl. apply (ringfromlt0 X is0 l). Defined.
Require Import UniMath.Algebra.Groups.