proposition: Lemma Rmult_le_compat_r : forall r r1 r2, 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
proof: Proof. now intros r r1 r2 H; rewrite 2(Rmult_comm _ r); apply Rmult_le_compat_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField