proposition: Lemma diff_xn_ub n (z x y: R): -z <= x -> x <= y -> y <= z -> `| y ^+ n - x ^+ n| <= (z^+(n.-1) *+ n) * (y - x).
proof: Proof. move => zx xy yz. rewrite subrXX mulrC normrM [`|_ - _|]ger0_norm ?ler_wpmul2r // ?subr_ge0 //. apply: (le_trans (ler_norm_sum _ _ _)). rewrite - [n in _*+ n] card_ord - sumr_const ler_sum // => [][i lin] _. rewrite normrM !normrX. have l1: 0<=`|x| <=z by rewrite normr_ge0 /= ler_norml zx /= (le_trans xy yz). have l2: 0<=`|y| <=z by rewrite normr_ge0 /= ler_norml yz /= (le_trans zx xy). have /andP [pa pb] := pow_monotone i l1. have /andP [pc pd] := pow_monotone (n.-1 - i)%N l2. by move: (ler_pmul pc pa pd pb); rewrite - exprD subnK //; move: lin; case n. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)