proposition: Lemma strong_mono_bound p a r : strong_mono p a r -> {k | 0 < k & forall x y, `|x - a| <= r -> `|y - a| <= r -> `| x - y | <= k * `| p.[x] - p.[y] | }.
proof: Proof. case=> [] [[k k_gt0 hk] _]; exists k^-1; rewrite ?invr_gt0=> // x y hx hy; have [->|neq_xy] := eqVneq x y; do ?[by rewrite !subrr normr0 mulr0]; move: (hk _ _ neq_xy hx hy); rewrite 1?ltr_oppr ler_pdivl_mull //; rewrite -ler_pdivl_mulr ?normr_gt0 ?subr_eq0 // => /ltW /le_trans-> //; by rewrite -normfV -normrM ler_normr lexx ?orbT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)