proposition: Theorem sqr_correct : forall u (Y : I.type) tf f, approximates Y tf f -> approximates Y (sqr u Y tf) (fun x => Xsqr (f x)).
proof: Proof. move=> u Y tf f Hf. apply: (@approximates_ext (fun x => Xpower_int (f x) 2%Z)). move=> x; rewrite /Xpower_int /Xsqr. case: (f x) =>[//|r]. by rewrite /= Rmult_1_r. exact: power_int_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