proposition: Lemma midpoint_correct : forall xi, not_empty (I.convert xi) -> I.convert (midpoint xi) = let m := Xreal (proj_val (I.F.convert (I.midpoint xi))) in Ibnd m m.
proof: Proof. intros xi Ex. destruct (I.midpoint_correct xi Ex) as [H1 H2]. unfold midpoint. rewrite I.bnd_correct. now rewrite H1. now apply I.valid_lb_real. now apply I.valid_ub_real. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic