fact: Parameter ComputeBound_correct : forall u pi p, pi >:: p -> J.extension (PolR.horner tt p) (ComputeBound u pi).
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval MathComp Datatypes