proposition: Lemma Rmult_lt_compat : forall a b c d, 0 < a -> 0 < b -> a < c -> b < d -> a * b < c * d.
proof: Proof. intros a b c d a_pos b_pos Hac Hdb ; transitivity (a * d). apply Rmult_lt_compat_l ; assumption. apply Rmult_lt_compat_r ; [transitivity b |] ; assumption. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rpser_sums_facts