proposition: Lemma subset_midpoint : forall xi, not_empty (I.convert xi) -> subset' (I.convert (midpoint xi)) (I.convert xi).
proof: Proof. intros xi Ex. rewrite (midpoint_correct xi Ex). intros [|x]. easy. intros [H1 H2]. rewrite (Rle_antisym _ _ H2 H1). destruct (I.midpoint_correct xi Ex) as [H3 H4]. now rewrite <- H3. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic