proposition: Lemma Derivative_I_mult : Derivative_I Hab' (F{*}G) (F{*}G'{+}F'{*}G).
proof: Proof. elim derF; intros incF H1. elim H1; intros incF' H2. elim derG; intros incG H5. elim H5; intros incG' H6. clear H5 H1. set (contF := deriv_imp_contin_I _ _ _ _ _ (less_leEq _ _ _ Hab') derF) in *. set (contG := deriv_imp_contin_I _ _ _ _ _ (less_leEq _ _ _ Hab') derG) in *. set (contG' := deriv_imp_contin'_I _ _ _ _ _ (less_leEq _ _ _ Hab') derG) in *. set (nF := Norm_Funct contF) in *. set (nG := Norm_Funct contG) in *. set (nG' := Norm_Funct contG') in *. apply Derivative_I_char. Contin. Contin. intros e He. set (M := Max (Max nF nG) nG'[+][1]) in *. cut ([0] [<] M). intro HM'. cut (M [#] [0]). intro HM. 2: apply Greater_imp_ap; assumption. cut (Three[*]M [#] [0]). intro H3M. 2: apply mult_resp_ap_zero; [ apply three_ap_zero | assumption ]. cut ([0] [<] (e[/] _[//]H3M)). intro HeM. elim (contin_prop _ _ _ _ contF _ HeM); intros dc H H0. elim (H2 _ HeM); intros df H1 H3. elim (H6 _ HeM); intros dg H4 H5. clear H2 H6. set (d := Min (Min df dg) dc) in *. exists d. unfold d in |- *; repeat apply less_Min; assumption. intros x y H2 H6 Hx Hy Hx' H7. simpl in |- *. 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 *. set (f'x := F' x (ProjIR1 (ProjIR2 Hx'))) in *. set (g'x := G' x (ProjIR2 (ProjIR1 Hx'))) in *. apply leEq_wdl with (AbsIR (fy[*]gy[-]fx[*]gx[-](fx[*]g'x[+]f'x[*]gx)[*](y[-]x))). 2: apply AbsIR_wd; unfold fx, f'x, gx, g'x in |- *; rational. apply leEq_wdl with (AbsIR (fy[*](gy[-]gx[-]g'x[*](y[-]x))[+](fy[-]fx)[*]g'x[*](y[-]x)[+] gx[*](fy[-]fx[-]f'x[*](y[-]x)))). astepr (e[*]AbsIR (y[-]x)). rstepr (e [/]ThreeNZ[*]AbsIR (y[-]x)[+]e [/]ThreeNZ[*]AbsIR (y[-]x)[+] e [/]ThreeNZ[*]AbsIR (y[-]x)). eapply leEq_transitive; [ apply triangle_IR | apply plus_resp_leEq_both ]. eapply leEq_transitive; [ apply triangle_IR | apply plus_resp_leEq_both ]. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (M[*]AbsIR (gy[-]gx[-]g'x[*](y[-]x))). apply mult_resp_leEq_rht; [ apply leEq_transitive with nF | apply AbsIR_nonneg ]. unfold nF, I, fy in |- *; apply norm_bnd_AbsIR. assumption. unfold M in |- *; eapply leEq_transitive. 2: apply less_leEq; apply less_plusOne. eapply leEq_transitive. 2: apply lft_leEq_Max. apply lft_leEq_Max. apply shift_mult_leEq' with HM. assumption. rstepr ((e[/] _[//]H3M)[*]AbsIR (y[-]x)). unfold gx, gy, g'x in |- *; apply H5; try assumption. apply leEq_transitive with d. assumption. unfold d in |- *; eapply leEq_transitive; [ apply Min_leEq_lft | 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. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (AbsIR (fy[-]fx)[*]M). apply mult_resp_leEq_lft. unfold M in |- *; eapply leEq_transitive. 2: apply less_leEq; apply less_plusOne. eapply leEq_transitive. 2: apply rht_leEq_Max. unfold nG', I, g'x in |- *; apply norm_bnd_AbsIR; assumption. apply AbsIR_nonneg. apply shift_mult_leEq with HM. assumption. rstepr (e[/] _[//]H3M). unfold fx, fy in |- *; apply H0; try assumption. apply leEq_transitive with d. 2: unfold d in |- *; apply Min_leEq_rht. eapply leEq_wdl. apply H7. apply AbsIR_minus. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (M[*]AbsIR (fy[-]fx[-]f'x[*](y[-]x))). apply mult_resp_leEq_rht; [ apply leEq_transitive with nG | apply AbsIR_nonneg ]. unfold nG, I, gx in |- *; apply norm_bnd_AbsIR; assumption. unfold M in |- *; eapply leEq_transitive. 2: apply less_leEq; apply less_plusOne. eapply leEq_transitive. 2: apply lft_leEq_Max. apply rht_leEq_Max. apply shift_mult_leEq' with HM. assumption. rstepr ((e[/] _[//]H3M)[*]AbsIR (y[-]x)). unfold fx, fy, f'x in |- *; apply H3; try assumption. apply leEq_transitive with d. assumption. unfold d in |- *; eapply leEq_transitive; [ apply Min_leEq_lft | apply Min_leEq_lft ]. apply AbsIR_wd; rational. apply div_resp_pos. astepl (Three[*]ZeroR); apply mult_resp_less_lft. assumption. apply pos_three. assumption. unfold M in |- *; eapply leEq_less_trans. 2: apply less_plusOne. eapply leEq_transitive. 2: apply rht_leEq_Max. unfold nG' in |- *; apply positive_norm. Qed.
imports: CoRN.ftc.Derivative