let r, L, a, b, t be Real; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: (((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; :: thesis: verum