proposition: Lemma contains_le : forall xl xu v, contains (Ibnd xl xu) v -> le_lower xl v /\ le_upper v xu.
proof: Proof. intros xl xu v. case v. intro. elim H. intros r. case xl. intro. exact H. intros l (Hl, Hu). split. exact (Ropp_le_contravar _ _ Hl). exact Hu. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic