Lemma isinvringmultgtif (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is1 : isringmultgt X R) (nc : neqchoice R) (isa : isasymm R) : isinvringmultgt X R. Proof. intros. split. - intros a b rab0 ra0. assert (int : b != 0). { intro e. rewrite e in rab0. rewrite (ringmultx0 X _) in rab0. apply (isa _ _ rab0 rab0). } induction (nc _ _ int) as [ g | l ]. + apply g. + set (int' := ringmultgt0lt0 X is0 is1 ra0 l). induction (isa _ _ rab0 int'). - intros a b rab0 rb0. assert (int : a != 0). { intro e. rewrite e in rab0. rewrite (ringmult0x X _) in rab0. apply (isa _ _ rab0 rab0). } induction (nc _ _ int) as [ g | l ]. + apply g. + set (int' := ringmultlt0gt0 X is0 is1 l rb0). induction (isa _ _ rab0 int'). Defined.
Require Import UniMath.Algebra.Groups.