fact: Definition eval_hyp_bnd (prec : I.precision) (h : hyp) := match h with | Hlele _ _ u v => I.join (E.eval_bnd prec u) (E.eval_bnd prec v) | Hle _ _ v => I.lower_extent (E.eval_bnd prec v) | Hge _ _ u => I.upper_extent (E.eval_bnd prec u) | Habsle _ _ v => let vi := I.lower_extent (E.eval_bnd prec v) in I.meet (I.neg vi) vi end.
imports: Coq(Reals Psatz) Flocq(Raux) Coq(List) Xreal Interval Tree Prog