proposition: Theorem round_flt_correct u m e p (Y : I.type) tf f : approximates Y tf f -> approximates Y (round_flt u m e p Y tf) (fun x => Xround_flt m e p (f x)).
proof: Proof. move=> Hf. rewrite /round_flt. apply: (@approximates_ext (fun x : R => Xadd (f x) (Xerror_flt m e p (f x)))). { move=> x. case: (f x) => //= xr. congr Xreal; rewrite /Basic.error_flt /Basic.round_flt. ring. } apply: add_correct => //=. exact: error_flt_correct. 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