proposition: Lemma deriv_imp_contin_I : Derivative_I Hab' F G -> Continuous_I Hab'' F.
proof: Proof. intro derF. elim derF; intros incF H2; elim H2; clear H2; intros incG deriv. split; auto. intros e He. elim deriv with e; auto. clear deriv; intros d posd Hd. set (contG := deriv_imp_contin'_I derF) in *. set (M := Norm_Funct contG) in *. set (D := Min d (Min ([1] [/]TwoNZ) (e[/] _[//] mult_resp_ap_zero _ _ _ (two_ap_zero IR) (max_one_ap_zero M)))) in *. exists D. unfold D in |- *; repeat apply less_Min. auto. apply (pos_half IR). apply div_resp_pos; auto. apply shift_less_mult' with (two_ap_zero IR). apply pos_two. astepl ZeroR. eapply less_leEq_trans. 2: apply rht_leEq_Max. apply pos_one. intros x y H0 H1 Hx Hy H2. apply leEq_wdl with (AbsIR (F x Hx[-]F y Hy[-]G y (incG _ H1) [*] (x[-]y) [+] G y (incG _ H1) [*] (x[-]y))). 2: apply AbsIR_wd; rational. eapply leEq_transitive. apply triangle_IR. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). apply plus_resp_leEq_both. apply leEq_transitive with (e[*]AbsIR (x[-]y)). apply Hd; auto. apply leEq_transitive with D. eapply leEq_wdl; [ apply H2 | apply AbsIR_minus ]. unfold D in |- *; apply Min_leEq_lft. rstepr (e[*][1] [/]TwoNZ). apply mult_resp_leEq_lft. apply leEq_transitive with D; auto. unfold D in |- *; eapply leEq_transitive; [ apply Min_leEq_rht | apply Min_leEq_lft ]. apply less_leEq; auto. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (Max M [1][*]AbsIR (x[-]y)). apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. eapply leEq_transitive. 2: apply lft_leEq_Max. unfold M in |- *; apply norm_bnd_AbsIR; auto. apply shift_mult_leEq' with (max_one_ap_zero M). eapply less_leEq_trans; [ apply pos_one | apply rht_leEq_Max ]. eapply leEq_wdr. eapply leEq_transitive. apply H2. unfold D in |- *. eapply leEq_transitive; apply Min_leEq_rht. rational. Qed.
imports: CoRN.ftc.Continuity