proposition: Lemma Rmult_lt_gt_compat_neg_l : forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
proof: Proof. intros r r1 r2 I%Ropp_lt_contravar J; rewrite Ropp_0 in I. now apply Ropp_lt_cancel; rewrite 2Ropp_mult_distr_l; apply Rmult_lt_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField