fact: Definition root_plain prec depth hyps px cx pf cf := let hyps := R.merge_hyps prec hyps in let xi := nth 0 (A.BndValuator.eval prec px (hyps ++ map (T.eval_bnd prec) cx)) I.nai in root_plain_aux depth prec pf (hyps ++ map (T.eval_bnd prec) cf) xi Eq.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify Interval_helper