let r, L, a, b, t be Real; for m being Nat st a <= t & t <= b & 0 <= L & 0 <= r holds
(((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * L <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * L
let m be Nat; ( a <= t & t <= b & 0 <= L & 0 <= r implies (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * L <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * L )
assume A1:
( a <= t & t <= b & 0 <= L & 0 <= r )
; (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * L <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * L
then
t - a <= b - a
by XREAL_1:13;
then A2:
r * (t - a) <= r * (b - a)
by A1, XREAL_1:64;
0 <= t - a
by A1, XREAL_1:48;
then A3:
(r * (t - a)) to_power (m + 1) <= (r * (b - a)) to_power (m + 1)
by A1, HOLDER_1:3, A2;
((r * (t - a)) |^ (m + 1)) / ((m + 1) !) <= ((r * (b - a)) |^ (m + 1)) / ((m + 1) !)
by A3, XREAL_1:72;
hence
(((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * L <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) !)) * L
by A1, XREAL_1:64; verum