proposition: Theorem sin_correct : forall u (Y : I.type) tf f, approximates Y tf f -> approximates Y (sin u Y tf) (fun x => Xsin (f x)).
proof: Proof. apply: fun_gen_correct =>//. - exact: I.sin_correct. - exact: size_TM_sin. - exact: TM_sin_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