fact: Definition extent e := match e with | ie_none => fun v => v | ie_lower => I.lower_extent | ie_upper => I.upper_extent end.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify