Definition intdomnonzerotopos (X : intdom) (R : hrel X) (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (is2 : R 1 0) (nc : neqchoice R) (x : intdomnonzerosubmonoid X) : ringpossubmonoid X is1 is2. Proof. intros. induction (nc (pr1 x) 0 (pr2 x)) as [ g | l ]. - apply (pr1 x ,, g). - exists (- pr1 x). simpl. apply ringtogt0. + apply is0. + rewrite (ringminusminus X _). apply l. Defined.
Require Import UniMath.Algebra.Groups.