Lemma ringmultgt0lt0 (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isringmultgt X R) {x y : X} (isx : R x 0) (isy : R 0 y) : R 0 (x * y). Proof. intros. set (isy' := grfromltunel X is0 isy). assert (r := is _ _ isx isy'). change (pr1 (R (x * (- y)) 0)) in r. rewrite (ringrmultminus X _ _) in r. assert (r' := grfromgtunel X is0 r). change (pr1 (R 0 (- - (x * y)))) in r'. rewrite (ringminusminus X (x * y)) in r'. apply r'. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.