proposition: Lemma Taylor_lemma7 : forall n Hf Hf' i (Hi : 0 < i) Hi', Derivative_I Hab' (funct_i' n Hf i Hi') (funct_aux n Hf' i Hi'{-}funct_aux n Hf' (pred i) (lt_5 i (S n) Hi')).
proof: Proof. do 5 intro. rewrite <- (Nat.lt_succ_pred _ _ Hi). set (p := pred i) in *; clearbody p; clear Hi i. intros. cut (Derivative_I Hab' (PartInt (fi n Hf _ Hi')) (PartInt (fi (S n) Hf' (S (S p)) (proj1 (Nat.succ_lt_mono _ _) Hi')))); [ intro | apply Taylor_lemma6 ]. unfold funct_aux, funct_i' in |- *. New_Deriv. apply Feq_reflexive. Lazy_Included. apply eq_imp_Feq. Lazy_Included. Lazy_Included. intros x X0 Hx Hx'. simpl in Hx, Hx'; simpl in |- *. set (fiSp1 := fi n Hf (S p) Hi') in *. set (fiSp2 := fi (S n) Hf' (S p) (proj1 (Nat.succ_lt_mono p (S n)) (lt_5 (S p) (S n) Hi'))) in *. cut (forall x y : subset I, scs_elem _ _ x [=] scs_elem _ _ y -> fiSp1 x [=] fiSp2 y); intros. set (x1 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR1 (ProjIR1 Hx)))) in *. simpl in (value of x1); fold x1 in |- *. set (x2 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR1 (ProjIR2 Hx')))) in *. simpl in (value of x2); fold x2 in |- *. set (x3 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR1 (ProjIR1 (ProjIR2 Hx))))) in *. simpl in (value of x3); fold x3 in |- *. set (x4 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR1 (ProjIR1 Hx')))) in *. simpl in (value of x4); fold x4 in |- *. set (x5 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR2 (ProjIR1 (ProjIR2 Hx))))) in *. simpl in (value of x5); fold x5 in |- *. set (fiSSp := fi (S n) Hf' (S (S p)) (proj1 (Nat.succ_lt_mono (S p) (S n)) Hi')) in *. set (pp := [1][/] nring (fact p + p * fact p) [//]nring_fac_ap_zero IR (S p)) in *. set (bxp := nexp _ p (b[-]x)) in *. set (a1 := fiSp1 x1) in *; set (a5 := fiSSp x5) in *; simpl in (value of a1), (value of a5); fold a1 a5 in |- *. rstepl (a5[*]pp[*] (bxp[*] (b[-]x)) [-]a1[*] ((nring p[+][1]) [*]pp) [*]bxp). unfold a1, a5 in |- *; clear a1 a5. Lazy_Eq. unfold x4, x5 in |- *; algebra. simpl in |- *; algebra. unfold pp in |- *. rstepr (nring (S p) [*] ([1][/] _[//] mult_resp_ap_zero _ _ _ (nring_fac_ap_zero _ p) (pos_ap_zero _ _ (pos_nring_S IR p)))); simpl in |- *. apply mult_wdr; apply div_wd. algebra. clear X H bxp pp x5 x4 x3 x2 x1 fiSSp fiSp1 fiSp2 Hx. cut (fact p + p * fact p = fact p * S p). intro; rewrite H. eapply eq_transitive_unfolded. apply nring_comm_mult. algebra. transitivity (S p * fact p); auto with arith. unfold fiSp1, fiSp2 in |- *. apply eq_transitive_unfolded with (PartInt (fi n Hf (S p) Hi') (scs_elem _ _ x0) (scs_prf _ _ x0)). 2: apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S p) (proj1 (Nat.succ_lt_mono _ _) (lt_5 _ _ Hi'))) (scs_elem _ _ x0) (scs_prf _ _ x0)). simpl in |- *; apply csf_wd_unfolded. case x0; simpl in |- *; algebra. apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with (S p) F; apply Taylor_lemma1. apply scs_prf. simpl in |- *; apply csf_wd_unfolded. generalize H; case x0; case y; auto. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)