fact: Definition pol_increasing (p : {poly R}) := {homo (horner p): x y / x <= y}.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol