fact: Definition check_width prec (w : F.type * bool) yi := let yl := I.lower yi in let yu := I.upper yi in let (f, r) := w in let w := if r then F.mul_UP prec (F.midpoint yl yu) f else f in F'.le' (F.sub_UP prec (I.upper yi) (I.lower yi)) f.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Coquelicot(Coquelicot) Stdlib Coquelicot Xreal Basic Sig Interval Integral Eval Bertrand Tree Prog Reify Refine Interval_helper