fact: Definition inv (p: {poly R}) := forall epsilon, 0 < epsilon -> { x | [/\ (le_below_x x (horner p)), {in <=%R x &, pol_increasing p} & (0 < 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