fact: Definition ComputeBound : Pol.U -> Pol.T -> I.type -> I.type := Pol.horner.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval MathComp Datatypes