fact: Definition le_below_x (x: R) (f: R -> R) := (forall y, 0 <= y -> y <= x -> f y <= f x).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol