proposition: Lemma Max_monotone : forall (f: PartIR), (forall (x y:IR) Hx Hy, (Min a b)[<=]x -> x[<=]y -> y[<=](Max a b) -> (f x Hx)[<=](f y Hy)) -> forall Ha Hb Hc, (Max (f a Ha) (f b Hb)) [=] f (Max a b) Hc.
proof: Proof. intros f H Ha Hb Hc. apply leEq_imp_eq. apply Max_leEq; apply H; (apply leEq_reflexive || apply Min_leEq_lft || apply Min_leEq_rht || apply lft_leEq_Max || apply rht_leEq_Max). rewrite -> leEq_def. intros X. apply (leEq_or_leEq IR a b). intros H0. generalize X; clear X. change (Not (Max (f a Ha) (f b Hb)[<]f (Max a b) Hc)). rewrite <- leEq_def. destruct H0. stepl (f b Hb). apply rht_leEq_Max. apply pfwdef. apply eq_symmetric; apply leEq_imp_Max_is_rht. assumption. stepl (f a Ha). apply lft_leEq_Max. apply pfwdef. stepr (Max b a). apply eq_symmetric; apply leEq_imp_Max_is_rht. assumption. now apply Max_comm. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq