proposition: Theorem const_correct (c : I.type) (r : R) : contains (I.convert c) (Xreal r) -> forall (X : I.type), approximates X (const c) (fun _ => Xreal r).
proof: Proof. move=> Hcr X. right. now exists (Xreal r). 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