proposition: Theorem TM_cst_correct (x0 : R) (ci X : I.type) (c : ExtendedR) : contains (I.convert X) (Xreal x0) -> contains (I.convert ci) c -> i_validTM x0 (I.convert X) (TM_cst X ci) (fun _ => c).
proof: Proof. move=> Hx0 Hc. split=>//=. move=> x Hx Nx. apply I.mask_propagate_r, contains_Xnan. by rewrite -Nx. by move=> HX; apply I.mask_propagate_l, I.mask_propagate_r. apply I.mask_correct', I.mask_correct', J.zero_correct. case: c Hc => [|c]; first move/contains_Xnan; move => Hc. exists (PolR.polyC 0%R); first by apply: Pol.polyC_correct; rewrite Hc. by move=> x Hx; rewrite I.mask_propagate_r. exists (PolR.polyC c); first exact: Pol.polyC_correct. move=> x Hx /=. rewrite Rmult_0_l Rplus_0_l Rminus_diag_eq //. apply I.mask_correct', I.mask_correct', J.zero_correct. 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