proposition: Lemma Rmult_ge_compat_l : forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2.
proof: Proof. now intros r r1 r2 I%Rge_le J%Rge_le; apply Rle_ge, Rmult_le_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField