fact: Definition inv2 (p : {poly R}) := forall epsilon, 0 < epsilon -> {x | [/\ (le_below_x x (horner p)), {in <=%R x &, pol_increasing p} & [&& 0 < x, 0 < p.[x] & x * p.[x] <= epsilon]] }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol