proposition: Theorem error_flt_correct u m e p (Y : I.type) tf f : approximates Y tf f -> approximates Y (error_flt u m e p Y tf) (fun x => Xerror_flt m e p (f x)).
proof: Proof. move=> Hf. rewrite /error_flt. set i := I.error_flt _ _ _ _. intros He x0. apply TM_any_correct. now apply contains_midpoint. intros x. destruct (f x) eqn:Hfx; move=> Hx /=. - rewrite {}/i contains_Xnan. apply J.error_flt_propagate. apply (eval_correct u) in Hf. apply Hf in Hx. simpl in Hx. rewrite Hfx in Hx. now apply contains_Xnan. - generalize (@eval_correct u Y tf f). move=> Haux. apply Haux in Hf. unfold I.extension in Hf. apply Hf in Hx. simpl in Hx. unfold Basic.round_flt. generalize (I.error_flt_correct u.1 m e p (eval u tf Y Y) (f x)). rewrite -/i /= {}/Xerror_flt {}/error_flt {}/Xbind Hfx. rewrite Hfx in Hx. now intros; revert Hx. 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