proposition: Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
proof: Proof. now intros r1 r2 I I'; rewrite <-(Rmult_0_l 0); apply Rmult_le_compat; try apply Rle_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField