proposition: Lemma Continuous_I_plus : Continuous_I Hab (F{+}G).
proof: Proof. clear incF incG. elim contF; intros incF' contF'. elim contG; intros incG' contG'. split. Included. intros. elim (contF' (e [/]TwoNZ)). elim (contG' (e [/]TwoNZ)). clear contF contG contF' contG'. 2: apply pos_div_two; assumption. 2: apply pos_div_two; assumption. intros df H0 H1 dg H2 H3. exists (Min df dg). apply less_Min; assumption. intros. simpl in |- *. apply leEq_wdl with (AbsIR (F x (ProjIR1 Hx) [-]F y (ProjIR1 Hy) [+] (G x (ProjIR2 Hx) [-]G y (ProjIR2 Hy)))). rstepr (e [/]TwoNZ[+]e [/]TwoNZ). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. simpl in |- *; apply H3; try assumption. apply leEq_transitive with (Min df dg); [ assumption | apply Min_leEq_rht ]. simpl in |- *; apply H1; try assumption. apply leEq_transitive with (Min df dg); [ assumption | apply Min_leEq_lft ]. apply AbsIR_wd; rational. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac