fact: Definition eval_goal (g : gol) (x : R) := match g with | Gle true v => (x <= eval v nil)%R | Gle false v => (eval v nil >= x)%R | Gge true u => (eval u nil <= x)%R | Gge false u => (x >= eval u nil)%R | Glele u v => (eval u nil <= x <= eval v nil)%R | Gltle u v => (eval u nil < x <= eval v nil)%R | Glelt u v => (eval u nil <= x < eval v nil)%R | Gltlt u v => (eval u nil < x < eval v nil)%R | Gabsle true v => (Rabs x <= eval v nil)%R | Gabsle false v => (eval v nil >= Rabs x)%R | Glt v => (x < eval v nil)%R | Ggt u => (eval u nil < x)%R | Gne true u => (x <> eval u nil) | Gne false u => (eval u nil <> x) end.
imports: Coq(Reals Psatz) Flocq(Raux) Coq(List) Xreal Interval Tree Prog