proposition: Lemma Continuous_I_max : Continuous_I Hab (FMax F G).
proof: Proof. clear incF incG. elim contF; intros incF contF'. elim contG; intros incG contG'. split. Included. intros e He. elim (contF' (e [/]TwoNZ) (pos_div_two _ _ He)); intros dF dFpos HdF. elim (contG' (e [/]TwoNZ) (pos_div_two _ _ He)); intros dG dGpos HdG. clear contF contG contF' contG'. exists (Min dF dG). apply less_Min; auto. intros x y Hx' Hy' Hx Hy Hxy. assert (AbsIR (x[-]y) [<=] dF). eapply leEq_transitive; [ apply Hxy | apply Min_leEq_lft ]. assert (AbsIR (x[-]y) [<=] dG). eapply leEq_transitive; [ apply Hxy | apply Min_leEq_rht ]. assert (HF := HdF x y Hx' Hy' (ProjIR1 Hx) (ProjIR1 Hy) H). assert (HG := HdG x y Hx' Hy' (ProjIR2 Hx) (ProjIR2 Hy) H0). Opaque AbsIR Max. simpl in |- *. Transparent AbsIR Max. set (Fx := F x (ProjIR1 Hx)) in *. set (Fy := F y (ProjIR1 Hy)) in *. set (Gx := G x (ProjIR2 Hx)) in *. set (Gy := G y (ProjIR2 Hy)) in *. elim (AbsIR_imp_AbsSmall _ _ HF); intros HF1 HF2. elim (AbsIR_imp_AbsSmall _ _ HG); intros HG1 HG2. apply leEq_wdl with (AbsIR (Max Fx Gx[-]Max Fx Gy[+] (Max Fx Gy[-]Max Fy Gy))). 2: apply AbsIR_wd; rational. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both; apply AbsSmall_imp_AbsIR; split. apply shift_zero_leEq_minus'. rstepr (e [/]TwoNZ[+]Max Fx Gx[-]Max Fx Gy). apply shift_zero_leEq_minus. apply Max_leEq. apply leEq_transitive with (e [/]TwoNZ[+]Fx). apply shift_leEq_plus; astepl ZeroR; apply less_leEq; apply pos_div_two; auto. apply plus_resp_leEq_lft; apply lft_leEq_Max. apply leEq_transitive with (e [/]TwoNZ[+]Gx). 2: apply plus_resp_leEq_lft; apply rht_leEq_Max. apply shift_leEq_plus. apply inv_cancel_leEq; rstepr (Gx[-]Gy); auto. apply shift_minus_leEq; apply Max_leEq. apply leEq_transitive with (e [/]TwoNZ[+]Fx). apply shift_leEq_plus; astepl ZeroR; apply less_leEq; apply pos_div_two; auto. apply plus_resp_leEq_lft; apply lft_leEq_Max. apply leEq_transitive with (e [/]TwoNZ[+]Gy). 2: apply plus_resp_leEq_lft; apply rht_leEq_Max. apply shift_leEq_plus; auto. apply shift_zero_leEq_minus'. rstepr (e [/]TwoNZ[+]Max Fx Gy[-]Max Fy Gy). apply shift_zero_leEq_minus. apply Max_leEq. apply leEq_transitive with (e [/]TwoNZ[+]Fx). apply shift_leEq_plus. apply inv_cancel_leEq; rstepr (Fx[-]Fy); auto. apply plus_resp_leEq_lft; apply lft_leEq_Max. apply leEq_transitive with (e [/]TwoNZ[+]Gy). 2: apply plus_resp_leEq_lft; apply rht_leEq_Max. apply shift_leEq_plus; astepl ZeroR; apply less_leEq; apply pos_div_two; auto. apply shift_minus_leEq; apply Max_leEq. apply leEq_transitive with (e [/]TwoNZ[+]Fy). apply shift_leEq_plus; auto. apply plus_resp_leEq_lft; apply lft_leEq_Max. apply leEq_transitive with (e [/]TwoNZ[+]Gy). apply shift_leEq_plus; astepl ZeroR; apply less_leEq; apply pos_div_two; auto. apply plus_resp_leEq_lft; apply rht_leEq_Max. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac