fact: Definition eval_RInt_contains prec deg limit hyps pf pu pv cf cu cv b := let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_init prec deg hyps pf pu pv cf cu cv in let check yi := I.subset yi b in check (IR.bisect prec limit mid Fi check).
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