fact: Definition eval_RInt_gen_infty_plain prec deg limit hyps mi pf pfm pu cf cfm cu w := let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps mi pf pfm pu cf cfm cu in IR.bisect prec limit mid Fi (check_width prec w).
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