proposition: Theorem eval_hyp_bnd_correct : forall prec h var, eval_hyp h var -> contains (I.convert (eval_hyp_bnd prec h)) (Xreal var).
proof: Proof. intros prec h var. destruct h as [b l v|b l u|l1 l2 u v|b l v] ; intros H. - apply I.lower_extent_correct with (eval v nil). apply E.eval_bnd_correct. destruct l ; [|apply Rlt_le] ; destruct b ; [|apply Rge_le| |] ; apply H. - apply I.upper_extent_correct with (eval u nil). apply E.eval_bnd_correct. destruct l ; [|apply Rlt_le] ; destruct b ; [|apply Rge_le| |] ; apply H. - apply J.join_correct with (eval u nil) (eval v nil). apply E.eval_bnd_correct. apply E.eval_bnd_correct. destruct l1, l2 ; split ; try apply H ; apply Rlt_le, H. - assert (H': (- eval v nil <= var <= eval v nil)%R). apply Rabs_le_inv. destruct l ; [|apply Rlt_le] ; destruct b ; [|apply Rge_le| |] ; apply H. apply I.meet_correct. rewrite <- (Ropp_involutive var). apply J.neg_correct. apply I.lower_extent_correct with (eval v nil). apply E.eval_bnd_correct. lra. apply I.lower_extent_correct with (eval v nil). apply E.eval_bnd_correct. apply H'. Qed.
imports: Coq(Reals Psatz) Flocq(Raux) Coq(List) Xreal Interval Tree Prog