proposition: Theorem eval_bnd_correct : forall prec e, contains (I.convert (eval_bnd prec e)) (Xreal (eval e nil)).
proof: Proof. intros prec. induction e as [n|o|o e1 IHe1|o e1 IHe1 e2 IHe2]. - apply contains_Inan, I.nai_correct. - apply nullary_bnd_correct. - now apply unary_bnd_correct. - now apply binary_bnd_correct. Qed.
imports: Coq(Reals List) Xreal Basic Interval