proposition: Lemma Taylor_lemma8 : forall n Hf Hf' Hi, Derivative_I Hab' (funct_i' n Hf 0 Hi) (funct_aux n Hf' 0 Hi).
proof: Proof. intros. cut (Derivative_I Hab' (PartInt (fi n Hf _ Hi)) (PartInt (fi (S n) Hf' 1 (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; simpl in |- *. apply eq_transitive_unfolded with (fi (S n) Hf' 1 (proj1 (Nat.succ_lt_mono _ _) Hi) (Build_subcsetoid_crr _ _ _ (ProjIR1 (ProjIR2 (ProjIR1 (ProjIR2 Hx))))) [*] ([1][/] _[//]nring_fac_ap_zero IR 0) [*][1]). simpl in |- *; rational. Lazy_Eq; simpl in |- *; algebra. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)