proposition: Theorem ln_correct : forall u (Y : I.type) tf f, approximates Y tf f -> approximates Y (ln u Y tf) (fun x => Xln (f x)).
proof: Proof. apply: fun_gen_correct =>//. - exact: I.ln_correct. - exact: size_TM_ln. - exact: TM_ln_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