proposition: Theorem Rmult_lt_compat : forall r1 r2 r3 r4, (0 <= r1)%R -> (0 <= r3)%R -> (r1 < r2)%R -> (r3 < r4)%R -> (r1 * r3 < r2 * r4)%R.
proof: Proof. intros r1 r2 r3 r4 Pr1 Pr3 H12 H34. apply Rle_lt_trans with (r1 * r4)%R. - apply Rmult_le_compat_l. + exact Pr1. + now apply Rlt_le. - apply Rmult_lt_compat_r. + now apply Rle_lt_trans with r3. + exact H12. Qed.
imports: Coq(Psatz Reals ZArith) Zaux