Lemma ringmultlt0gt0 (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isringmultgt X R) {x y : X} (isx : R 0 x) (isy : R y 0) : R 0 (x * y). Proof. intros. set (isx' := grfromltunel X is0 isx). assert (r := is _ _ isx' isy). change (pr1 (R ((- x) * y) 0)) in r. rewrite (ringlmultminus 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.