proposition: Lemma slope_product_x (f : R -> R) x k: 0 <= x -> 0 <= k -> slope_bounded x k f -> forall y z, x <= y <= z -> (x * k + f y) * (z - y) <= z * f z - y * f y.
proof: Proof. rewrite /slope_bounded; move =>x0 kf0 incf y z /andP [xy yz]. rewrite -[z * _] (addrNK (z * f y)) -mulrBr -addrA -mulrBl mulrDl (mulrC (f y)). move: (le_trans xy yz) => xz. rewrite ler_add2r; apply: le_trans (_ : z * (k * (z - y)) <= _). by rewrite - mulrA ler_wpmul2r // mulr_ge0 // subr_ge0. by rewrite ler_wpmul2l ? incf ?xy ? yz//;apply:(le_trans x0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol