proposition: Lemma Rmult_le_ge_compat_neg_l : forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2.
proof: Proof. now intros r r1 r2 H I; apply Rle_ge, Rmult_le_compat_neg_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField