proposition: Lemma Taylor_lemma9 : forall n Hf Hf', Derivative_I Hab' (Taylor_seq'_aux n Hf) (funct_aux n Hf' n (Nat.lt_succ_diag_r n)).
proof: Proof. intro; induction n as [| n Hrecn]. intros. unfold Taylor_seq'_aux in |- *; simpl in |- *. apply Derivative_I_wdl with (funct_i' 0 Hf 0 (Nat.lt_succ_diag_r 0)). apply eq_imp_Feq. split; split; simpl in |- *; auto. split; split; split; simpl in |- *; auto. intros; simpl in |- *. apply eq_transitive_unfolded with ([0][+] fi 0 Hf 0 (Nat.lt_succ_diag_r 0) (Build_subcsetoid_crr _ _ _ (ProjIR1 (ProjIR1 Hx))) [*] ([1][/] [0][+][1][//]nring_fac_ap_zero IR 0) [*][1]). simpl in |- *; rational. Lazy_Eq; simpl in |- *; algebra. apply Taylor_lemma8; assumption. cut {p : nat | S n = p}; [ intro H | exists (S n); auto ]. elim H; intros p H0. rewrite H0. intros. unfold Taylor_seq'_aux in |- *; simpl in |- *. generalize Hf Hf'; clear Hf Hf'. rewrite <- H0; intros. cut (Diffble_I_n Hab' n F); [ intro H1 | apply le_imp_Diffble_I with (S n); [ lia | assumption ] ]. apply Derivative_I_wdl with (Taylor_seq'_aux n H1{+}funct_i' _ Hf _ (Nat.lt_succ_diag_r (S n))). unfold Taylor_seq'_aux in |- *. apply eq_imp_Feq. repeat (split; auto). try rename X into H2. apply FSumx_pred'. red in |- *; intros. try rename X into H6. exact (Taylor_lemma3' _ _ _ _ H3 _ _ _ _ H4 H6). intros; simpl in |- *; repeat (split; auto). repeat (split; auto). try rename X into H2. apply FSumx_pred'. red in |- *; intros. try rename X into H6. exact (Taylor_lemma3' _ _ _ _ H3 _ _ _ _ H4 H6). intros; simpl in |- *; repeat (split; auto). intros x H2 Hx Hx'; simpl in |- *. repeat first [ simple apply mult_wd | simple apply bin_op_wd_unfolded | simple apply csf_wd_unfolded | simple apply eq_reflexive_unfolded ]; simpl in |- *. 3: algebra. apply Feq_imp_eq with (Compact Hab). 2: assumption. apply FSumx_wd'. intros; apply eq_imp_Feq. repeat (split; auto). repeat (split; auto). intros x0 H4; intros; simpl in |- *. repeat apply mult_wdl. apply eq_transitive_unfolded with (PartInt (fi n H1 i (Nat.lt_lt_succ_r _ _ H3)) x0 H4). simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply eq_transitive_unfolded with (PartInt (fi (S n) Hf i (Nat.lt_lt_succ_r _ _ (Nat.lt_lt_succ_r _ _ H'))) x0 H4). 2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with i F; apply Taylor_lemma1. auto. apply eq_transitive_unfolded with (PartInt (fi n H1 n (Nat.lt_succ_diag_r _)) x H2). 2: apply eq_transitive_unfolded with (PartInt (fi (S n) Hf n (Nat.lt_lt_succ_r _ _ (Nat.lt_succ_diag_r _))) x H2). simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. 2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with n F; apply Taylor_lemma1. auto. apply Derivative_I_wdr with (funct_aux (S n) Hf' (pred (S n)) (lt_5 _ _ (Nat.lt_succ_diag_r (S n))) {+} (funct_aux _ Hf' _ (Nat.lt_succ_diag_r (S n)) {-} funct_aux (S n) Hf' (pred (S n)) (lt_5 _ _ (Nat.lt_succ_diag_r (S n))))). Opaque funct_aux. FEQ. Transparent funct_aux. repeat (split; auto). repeat (split; auto). apply Derivative_I_plus. apply Derivative_I_wdr with (funct_aux n Hf n (Nat.lt_succ_diag_r n)). apply eq_imp_Feq. repeat (split; auto). repeat (split; auto). intros x H2 Hx Hx'; simpl in |- *. repeat apply mult_wdl. apply eq_transitive_unfolded with (PartInt (fi (S n) Hf (S n) (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_succ_diag_r _))) x H2). 2: apply eq_transitive_unfolded with (PartInt (fi (S (S n)) Hf' (S n) (proj1 (Nat.succ_lt_mono _ _) (lt_5 _ _ (Nat.lt_succ_diag_r (S n))))) x H2). simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. 2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with (S n) F; apply Taylor_lemma1. auto. apply Hrecn. apply Taylor_lemma7. lia. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)