proposition: Lemma bounded_ex {xi} (Hne : not_empty (I.convert xi)) (Hbnded : I.bounded xi) : (exists l u : R, I.convert xi = Ibnd (Xreal l) (Xreal u)).
proof: Proof. exists (proj_val (I.F.convert (I.lower xi))). exists (proj_val (I.F.convert (I.upper xi))). have := (I.bounded_correct xi). rewrite Hbnded; case => // . move => Hlb Hub. case: (I.lower_bounded_correct xi Hlb) => <- => /= HbndedProp. case: (I.upper_bounded_correct xi Hub) => <-. by rewrite /I.bounded_prop; apply. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl