defpred S1[ Nat] means $1 ^2 <= 2 * ((($1 ^2) - $1) + 1);
A1: for k being Nat st k >= 1 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 1 & S1[k] implies S1[k + 1] )
assume that
A2: k >= 1 and
A3: k ^2 <= 2 * (((k ^2) - k) + 1) ; :: thesis: S1[k + 1]
A4: (k ^2) + ((2 * k) + 1) <= (2 * (((k ^2) - k) + 1)) + ((2 * k) + 1) by A3, XREAL_1:6;
2 * k >= 2 * 1 by A2, XREAL_1:64;
then (2 * k) + 2 >= 2 + 2 by XREAL_1:6;
then A5: (2 * (k ^2)) + 4 <= (2 * (k ^2)) + ((2 * k) + 2) by XREAL_1:6;
(2 * (k ^2)) + 3 <= (2 * (k ^2)) + 4 by XREAL_1:6;
then (2 * (((k ^2) - k) + 1)) + ((2 * k) + 1) <= (2 * (k ^2)) + ((2 * k) + 2) by A5, XXREAL_0:2;
hence S1[k + 1] by A4, XXREAL_0:2; :: thesis: verum
end;
A6: S1[1] ;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A6, A1);
 hence for n being Element of NAT st n >= 1 holds
n ^2 <= 2 * (((n ^2) - n) + 1) ; :: thesis: verum