proposition: Lemma diff_xn_ub {R : archiFieldType} (n : nat) : forall z, (0 < z)%R -> exists2 k, (0 <= k)%R & forall x y : R, (0 < x)%R -> x <= y -> (y <= z) -> y ^+ n - x ^+ n <= k * (y - x).
proof: Proof. elim: n => [z z0| n IHn z z0]. by exists 0%R => // x y x0 xy yz; rewrite !expr0 subrr mul0r. have [k k0 kp] := IHn z z0. exists (z * k + z ^+ n) => [| x y x0 xy yz]. by rewrite addr_ge0// ?exprn_ge0// ?mulr_ge0// ltW. rewrite !exprS. rewrite (_: _ * _ - _ = y * (y ^+ n - x ^+ n) + (y - x) * x ^+ n); last first. by rewrite mulrDr mulrDl addrA mulrN mulNr addrNK. rewrite [_ * (y-x)]mulrDl ler_add //=. rewrite -mulrA (@le_trans _ _ (y * (k * (y - x))))//. rewrite (ler_wpmul2l (le_trans (ltW x0) xy))//. exact: kp. by rewrite !(mulrCA _ k) ler_wpmul2l// ler_wpmul2r// subr_ge0. rewrite (mulrC (_ - _)) ler_wpmul2r ?subr_ge0// ler_expn2r//. - by rewrite nnegrE ltW. - by rewrite nnegrE ltW. - exact: le_trans yz. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc