Lemma ringmultlt0lt0 (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isringmultgt X R) {x y : X} (isx : R 0 x) (isy : R 0 y) : R (x * y) 0. Proof. intros. set (rx := ringfromlt0 _ is0 isx). assert (ry := ringfromlt0 _ is0 isy). assert (int := is _ _ rx ry). rewrite (ringmultminusminus X _ _) in int. apply int. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.