proposition: Lemma get_tm_correct u Y tf f : approximates Y tf f -> approximates Y (Tm (get_tm u Y tf)) f.
proof: Proof. case: tf =>[c||tm]; rewrite /approximates // => H Hne. move/(_ Hne) in H. - destruct H as [H|H]. split ; intros ; rewrite ?I.mask_propagate_r //. exact: contains_midpoint. exists (PolR.polyC 0). now apply Pol.polyC_correct ; rewrite H. easy. apply TM_cst_correct_strong =>//. exact: contains_midpoint. - apply: TM_var_correct_strong=>//. exact: J.subset_midpoint. exact: J.contains_midpoint. - exact: H. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig