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

proof

let k be non trivial Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
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: verum

end;

assume n > 1 ; :: thesis: (((4 * n) * n) - (2 * n)) / (n + 1) > 1
then A3: not n is trivial by NAT_2:28;
A4: S₁[2] ;
for k being non trivial Nat holds S₁[k] from NAT_2:sch 2(A4, A1);
hence (((4 * n) * n) - (2 * n)) / (n + 1) > 1 by A3; :: thesis: verum