fact: Definition bertrand_infty_interval alpha beta prec ui := if F'.le' c1 (I.lower ui) then BI.f_int_fast prec ui alpha beta else I.nai.
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