proposition: Lemma le_contains : forall xl xu v, le_lower xl (Xreal v) -> le_upper (Xreal v) xu -> contains (Ibnd xl xu) (Xreal v).
proof: Proof. intros xl xu v. case xl. intros _ Hu. exact (conj I Hu). intros l Hl Hu. split. exact (Ropp_le_cancel _ _ Hl). exact Hu. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic