proposition: Lemma TL_lemma_a' : forall n Hf, Dom (Taylor_seq'_aux n Hf) a.
proof: Proof. intros. split. apply FSumx_pred'. red in |- *; intros. simpl in X. inversion_clear X. inversion_clear X0. simpl in |- *. split; split; auto. apply compact_wd with x; auto. intros. apply TL_a_i'. apply TL_a_i'. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)