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