proposition: Lemma contains_midpoint : forall X : I.type, not_empty (I.convert X) -> contains (I.convert X) (Xreal (proj_val (I.F.convert (I.midpoint X)))).
proof: Proof. intros X H. destruct (I.midpoint_correct X H) as [H1 H2]. now rewrite <- H1. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig