proposition: Lemma Taylor_lemma6 : forall n Hf Hf' i Hi, Derivative_I Hab' (PartInt (fi n Hf i Hi)) (PartInt (fi (S n) Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi))).
proof: Proof. intros. cut (Derivative_I_n Hab' 1 (PartInt (fi n Hf i Hi)) (PartInt (fi (S n) Hf' (S i) (proj1 (Nat.succ_lt_mono i (S n)) Hi)))). intro H. simpl in H. elim H; intros f' H1 H2. apply Derivative_I_wdr with (PartInt f'); assumption. cut (S i = 1 + i); [ intro | lia ]. cut (1 + i < S (S n)); [ intro | lia ]. apply Derivative_I_n_wdr with (PartInt (fi (S n) Hf' _ H0)). apply Derivative_I_n_unique with (S i) F. generalize H0; clear H0. rewrite <- H; intro. apply Taylor_lemma1. apply Taylor_lemma1. apply Derivative_I_n_wdl with (n_deriv_I _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (proj1 (Nat.lt_succ_r i n) Hi) _ Hf)). 2: apply Derivative_I_n_wdr with (n_deriv_I _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (proj1 (Nat.lt_succ_r _ _) H0) _ Hf')). 3: apply n_deriv_plus. apply Derivative_I_n_unique with i F. apply n_deriv_lemma. apply Taylor_lemma1. apply Derivative_I_n_unique with (1 + i) F. apply n_deriv_lemma. apply Taylor_lemma1. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)