proposition: Theorem TM_cst_correct_strong (x0 : R) (ci X : I.type) (f : R -> ExtendedR) : contains (I.convert X) (Xreal x0) -> is_const f (I.convert X) (I.convert ci) -> i_validTM x0 (I.convert X) (TM_cst X ci) f.
proof: Proof. move=> Hx0 [c H1 H2]. apply: TM_fun_eq; last apply: TM_cst_correct Hx0 H1. move=> x Hx /=. by apply sym_eq, H2. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound