proposition: Lemma max_mult : forall (a b c : IR), [0] [<=] c -> (Max (c[*]a) (c[*]b)) [=] c[*](Max a b).
proof: Proof. intros a b c H. apply leEq_imp_eq. apply Max_leEq; apply mult_resp_leEq_lft. apply lft_leEq_Max. assumption. apply rht_leEq_Max. assumption. rewrite -> leEq_def in *. intros Z. assert (Not (Not ([0][<]c or [0][=]c))). intros X. apply X. right. apply not_ap_imp_eq. intros Y. destruct (ap_imp_less _ _ _ Y) as [Y0|Y0]. auto. auto. apply H0. intros X. generalize Z. clear H H0 Z. change (Not (Max (c[*]a) (c[*]b)[<]c[*]Max a b)). rewrite <- leEq_def. destruct X as [c0|c0]. assert (X:c[#][0]). apply ap_symmetric; apply less_imp_ap; assumption. apply shift_mult_leEq' with X. assumption. apply Max_leEq;(apply shift_leEq_div;[assumption|]). rstepl (c[*]a); apply lft_leEq_Max. rstepl (c[*]b); apply rht_leEq_Max. stepl (c[*]a). apply lft_leEq_Max. csetoid_rewrite_rev c0. rational. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq