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