proposition: Lemma Derivative_I_comp : Derivative_I Hab' (G[o]F) ((G'[o]F) {*}F').
proof: Proof. elim derF; intros incF H1. elim H1; intros incF' H2. elim derG; intros incG H4. elim H4; intros incG' H5. clear H1 H4. apply Derivative_I_char. exact (included_comp _ _ _ _ _ _ _ _ incF incG Hmap). exact (included_FMult _ _ _ _ (included_comp _ _ _ _ _ _ _ _ incF incG' maps') incF'). intros e He. set (contF' := deriv_imp_contin'_I _ _ _ _ _ Hab derF) in *. set (nF' := Norm_Funct contF') in *. cut ([0] [<] [1][+]nF'). intro H. cut ([1][+]nF'[#][0]). intro HnF'. 2: apply Greater_imp_ap; assumption. set (alpha := ([1][/] _[//]HnF') [*]e [/]TwoNZ) in *. set (contG' := deriv_imp_contin'_I _ _ _ _ _ Hcd derG) in *. set (nH' := Norm_Funct contG') in *. cut ([0] [<] alpha). intro Halpha. cut ([0] [<] alpha[+]nH'). intro H0. cut (alpha[+]nH'[#][0]). intro HnH'. 2: apply Greater_imp_ap; assumption. set (beta := ([1][/] _[//]HnH') [*]e [/]TwoNZ) in *. cut ([0] [<] beta). intro Hbeta. elim (H2 _ Hbeta). intros df H1 H3. elim (H5 _ Halpha). intros dg H4 H6. elim (contin_prop _ _ _ _ (deriv_imp_contin_I _ _ _ _ _ Hab derF) _ H4). intros dc H7 H8. exists (Min dc df). apply less_Min; assumption. intros x y H9 H10 Hx Hy Hx' H11. simpl in |- *. set (fx := F x (ProjT1 Hx)) in *. set (fy := F y (ProjT1 Hy)) in *. set (gfx := G fx (ProjT2 Hx)) in *. set (gfy := G fy (ProjT2 Hy)) in *. set (fx' := F' x (ProjIR2 Hx')) in *. set (gfx' := G' (F x (ProjT1 (ProjIR1 Hx'))) (ProjT2 (ProjIR1 Hx'))) in *. simpl in (value of fx'), (value of gfx'); fold fx' gfx' in |- *. apply leEq_wdl with (AbsIR (gfy[-]gfx[-]gfx'[*] (fy[-]fx) [+]gfx'[*] (fy[-]fx[-]fx'[*] (y[-]x)))). 2: apply AbsIR_wd; rational. eapply leEq_transitive. apply triangle_IR. apply leEq_transitive with (alpha[*]nF'[*]AbsIR (y[-]x) [+]alpha[*]AbsIR (fy[-]fx[-]fx'[*] (y[-]x)) [+] nH'[*]AbsIR (fy[-]fx[-]fx'[*] (y[-]x))). apply plus_resp_leEq_both. apply leEq_transitive with (alpha[*]AbsIR (fy[-]fx)). unfold gfx' in |- *. cut (Dom G' fx). intro H12. apply leEq_wdl with (AbsIR (gfy[-]gfx[-]G' fx H12[*] (fy[-]fx))). unfold gfy, gfx in |- *; apply H6; unfold fx, fy in |- *. apply maps_lemma with G a b Hab; assumption. apply maps_lemma with G a b Hab; assumption. apply H8; try assumption. eapply leEq_transitive. apply H11. apply Min_leEq_lft. apply AbsIR_wd; unfold fx, fy, gfx, gfy in |- *; rational. apply (dom_wd _ G' _ fx (ProjT2 (ProjIR1 Hx'))). unfold fx in |- *; rational. rstepr (alpha[*] (nF'[*]AbsIR (y[-]x) [+]AbsIR (fy[-]fx[-]fx'[*] (y[-]x)))). apply mult_resp_leEq_lft. 2: apply less_leEq; assumption. apply leEq_wdl with (AbsIR (fx'[*] (y[-]x) [+] (fy[-]fx[-]fx'[*] (y[-]x)))). 2: apply un_op_wd_unfolded; rational. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. unfold fx', nF', I in |- *; apply norm_bnd_AbsIR; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. unfold gfx', nH' in |- *; apply norm_bnd_AbsIR; apply maps_lemma with G a b Hab; assumption. rstepl (alpha[*]nF'[*]AbsIR (y[-]x) [+] (alpha[+]nH') [*]AbsIR (fy[-]fx[-]fx'[*] (y[-]x))). rstepr (e [/]TwoNZ[*]ABSIR (y[-]x) [+]e [/]TwoNZ[*]ABSIR (y[-]x)). apply plus_resp_leEq_both. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. unfold alpha in |- *. rstepl ((nF'[/] _[//]HnF') [*]e [/]TwoNZ). astepr ([1][*]e [/]TwoNZ). apply mult_resp_leEq_rht. 2: apply less_leEq; apply pos_div_two; assumption. apply shift_div_leEq'. apply leEq_less_trans with nF'. unfold nF' in |- *; apply positive_norm. astepr (nF'[+][1]); apply less_plusOne. apply less_leEq; rstepr (nF'[+][1]); apply less_plusOne. apply shift_mult_leEq' with HnH'. assumption. apply leEq_wdr with (beta[*]ABSIR (y[-]x)). 2: unfold beta in |- *; rational. unfold fx, fy, fx' in |- *; apply H3; try assumption. eapply leEq_transitive. apply H11. apply Min_leEq_rht. unfold beta in |- *. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive. apply recip_resp_pos; assumption. apply pos_div_two; assumption. apply leEq_less_trans with nH'. unfold nH' in |- *; apply positive_norm. astepl ([0][+]nH'); apply plus_resp_less_rht; assumption. unfold alpha in |- *. astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive. apply recip_resp_pos; assumption. apply pos_div_two; assumption. apply leEq_less_trans with nF'. unfold nF' in |- *; apply positive_norm. astepr (nF'[+][1]); apply less_plusOne. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries