proposition: Lemma is_const_ext (f g : R -> ExtendedR) (X c : interval) : (forall x : R, contains X (Xreal x) -> f x = g x) -> is_const f X c -> is_const g X c.
proof: Proof. move=> Hmain [a Ha1 Ha2]. exists a =>//. move=> x Hx. rewrite -Hmain //. exact: Ha2. 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