proposition: 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: 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). } destruct (nc _ _ int) as [ g | l ]. + apply g. + set (int' := ringmultgt0lt0 X is0 is1 ra0 l). destruct (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). } destruct (nc _ _ int) as [ g | l ]. + apply g. + set (int' := ringmultlt0gt0 X is0 is1 l rb0). destruct (isa _ _ rab0 int'). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings