defpred S₁[ Nat] means (((4 * $1) * $1) - (2 * $1)) / ($1 + 1) > 1;
let n be Nat; :: thesis:
A1: for k being non trivial Nat st S₁[k] holds
S₁[k + 1]

let k be non trivial Nat; :: thesis:
assume A2: S₁[k] ; :: thesis:
set k1 = k + 1;
(((4 * k) * k) - (2 * k)) / (k + 1) = (((4 * k) * k) - (2 * k)) * (1 / (k + 1)) by XCMPLX_1:99;
then ((((4 * k) * k) - (2 * k)) * (1 / (k + 1))) * (k + 1) > 1 * (k + 1) by A2, XREAL_1:68;
then ((4 * k) * k) - (2 * k) > 1 * (k + 1) by XCMPLX_1:109;
then (((4 * k) * k) - (2 * k)) - (k + 1) > 0 by XREAL_1:50;
then ((((4 * k) * k) - (3 * k)) - 1) + ((8 * k) + 1) > 0 + 0 ;
then ((((4 * (k + 1)) * (k + 1)) - (2 * (k + 1))) - ((k + 1) + 1)) + ((k + 1) + 1) > 0 + ((k + 1) + 1) by XREAL_1:8;
then (((4 * (k + 1)) * (k + 1)) - (2 * (k + 1))) / ((k + 1) + 1) > ((k + 1) + 1) / ((k + 1) + 1) by XREAL_1:74;
hence S₁[k + 1] by XCMPLX_1:60; :: thesis:

end;