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