proposition: Lemma Derivative_I_recip : Derivative_I Hab' {1/}F {--} (F'{/}F{*}F).
proof: Proof. cut (forall (x : IR) (Hx : I x) Hx', F x Hx' [#] [0]). cut (forall (x : IR) (Hx : I x) Hx', (F{*}F) x Hx' [#] [0]). intros Hff Hf. clear derG. elim derF; intros incF H1. elim H1; intros incF' H2. assert (contF := deriv_imp_contin_I _ _ _ _ _ Hab derF). assert (contF' := deriv_imp_contin'_I _ _ _ _ _ Hab derF). assert (contF_ := contin_prop _ _ _ _ contF). clear H1. apply Derivative_I_char. Contin. Contin. intros e He. cut (Continuous_I Hab {1/}F); [ intro H | Contin ]. set (nF1 := Norm_Funct H) in *. set (nF' := Norm_Funct contF') in *. set (M := Max nF1 nF'[+][1]) in *. cut ([0] [<] M). intro HM. cut (M [#] [0]). intro H0. 2: apply Greater_imp_ap; assumption. cut (Two[*]M[*]M [#] [0]). intro HM2. cut (Two[*]M[*]M[*]M[*]M [#] [0]). intro HM4. cut ([0] [<] (e[/] _[//]HM2)). intro HeM2. cut ([0] [<] (e[/] _[//]HM4)). intro HeM4. elim (contF_ _ HeM4). intros d1 H1 H3. elim (H2 _ HeM2). intros d2 H4 H5. clear H2. exists (Min d1 d2). apply less_Min; assumption. intros x y H2 H6 Hx Hy Hx' H7. cut (forall (x : IR) (Hx : I x) Hx', AbsIR ([1][/] _[//]Hf x Hx Hx') [<=] M). intro leEqM. 2: intros z Hz Hz'. 2: apply leEq_wdl with (AbsIR ( {1/}F z (contin_imp_inc _ _ _ _ H z Hz))). 2: unfold M in |- *; eapply leEq_transitive. 3: apply less_leEq; apply less_plusOne. 2: eapply leEq_transitive. 3: apply lft_leEq_Max. 2: unfold nF1 in |- *; apply norm_bnd_AbsIR; assumption. 2: apply AbsIR_wd; simpl in |- *; algebra. cut (Dom F x); [ intro Hxx | simpl in Hx; unfold extend in Hx; inversion_clear Hx; assumption ]. cut (Dom F y); [ intro Hyy | simpl in Hy; unfold extend in Hy; inversion_clear Hy; assumption ]. cut (Dom F' x); [ intro Hxx' | simpl in Hx'; unfold extend in Hx'; inversion_clear Hx'; assumption ]. apply leEq_wdl with (AbsIR (([1][/] _[//]Hf y H6 Hyy)[-]([1][/] _[//]Hf x H2 Hxx)[+] (F' x Hxx'[/] _[//] mult_resp_ap_zero _ _ _ (Hf x H2 Hxx) (Hf x H2 Hxx))[*]( y[-]x))). apply leEq_wdl with (AbsIR ([--]([1][/] _[//]mult_resp_ap_zero _ _ _ (Hf x H2 Hxx) (Hf y H6 Hyy))[*] (F y Hyy[-]F x Hxx[-]F' x Hxx'[*](y[-]x)[+] F' x Hxx'[*](F x Hxx[-]F y Hyy[/] _[//]Hf x H2 Hxx)[*](y[-]x)))). 2: apply AbsIR_wd; rational. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. rstepr (M[*]M[*]((e[/] _[//]mult_resp_ap_zero _ _ _ H0 H0)[*]AbsIR (y[-]x))). apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_wdl. 2: apply AbsIR_inv. apply leEq_wdl with (AbsIR (([1][/] _[//]Hf x H2 Hxx)[*]([1][/] _[//]Hf y H6 Hyy))). 2: apply AbsIR_wd; rational. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg; apply leEqM. eapply leEq_transitive. apply triangle_IR. rstepr ((e[/] _[//]HM2)[*]AbsIR (y[-]x)[+](e[/] _[//]HM2)[*]AbsIR (y[-]x)). apply plus_resp_leEq_both. apply H5; try assumption. eapply leEq_transitive. apply H7. apply Min_leEq_rht. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_rht. 2: apply AbsIR_nonneg. apply leEq_wdl with (AbsIR ((F x Hxx[-]F y Hyy)[*](F' x Hxx'[/] _[//]Hf x H2 Hxx))). 2: apply AbsIR_wd; rational. rstepr ((e[/] _[//]HM4)[*](M[*]M)). eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. apply H3; try assumption. eapply leEq_transitive. apply H7. apply Min_leEq_lft. apply leEq_wdl with (AbsIR (F' x Hxx'[*]([1][/] _[//]Hf x H2 Hxx))). 2: apply AbsIR_wd; rational. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. unfold M in |- *; eapply leEq_transitive. 2: apply less_leEq; apply less_plusOne. eapply leEq_transitive. 2: apply rht_leEq_Max. unfold nF' in |- *; apply norm_bnd_AbsIR; assumption. apply leEqM. apply AbsIR_wd. simpl in |- *; rational. apply div_resp_pos. repeat (astepl (ZeroR[*][0]); apply mult_resp_less_both); try apply leEq_reflexive; try assumption. apply pos_two. assumption. apply div_resp_pos. repeat (astepl (ZeroR[*][0]); apply mult_resp_less_both); try apply leEq_reflexive; try assumption. apply pos_two. assumption. repeat apply mult_resp_ap_zero; try assumption. apply two_ap_zero. repeat apply mult_resp_ap_zero; try assumption. apply two_ap_zero. unfold M in |- *; eapply leEq_less_trans. 2: apply less_plusOne. eapply leEq_transitive. 2: apply lft_leEq_Max. unfold nF1 in |- *; apply positive_norm. intros. apply bnd_imp_ap_zero with I; auto. unfold I in |- *; Included. intros. apply bnd_imp_ap_zero with I; auto. Qed.
imports: CoRN.ftc.Derivative