fact: Definition one_root1 (p : {poly R}) (a b : R) := exists c d k, [/\ [&& a < c, c < d, d < b & 0 < k], (pos_in_interval a c (horner p)), (neg_in_interval1 d b (horner p)) & (slope_bounded2 c d k (horner p))].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol