proposition: Lemma contains_midpoint : forall xi, not_empty (I.convert xi) -> contains (I.convert (midpoint xi)) (Xreal (proj_val (I.F.convert (I.midpoint xi)))).
proof: Proof. intros xi Hx. rewrite (midpoint_correct xi Hx). split ; apply Rle_refl. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic