proposition: Lemma contains_le : forall xi x, contains (I.convert xi) x -> le_lower (I.F.convert (I.lower xi)) x /\ le_upper x (I.F.convert (I.upper xi)).
proof: Proof. intros xi x H. assert (H' := not_empty_contains _ _ H). rewrite I.lower_correct, I.upper_correct by easy. destruct I.convert as [|xl xu]. easy. now apply contains_le. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic