proposition: 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: Proof. intros. set (rx := ringfromlt0 _ is0 isx). assert (ry := ringfromlt0 _ is0 isy). assert (int := is _ _ rx ry). rewrite (ringmultminusminus X _ _) in int. apply int. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids