defpred S₁[ Nat] means 2 * $1 <= 2 to_power $1;
P1: S₁[ 0 ] ;
P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A1: S₁[n] ; :: thesis: S₁[n + 1]

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: S₁[n + 1]

hence 2 * (n + 1) <= 2 to_power (n + 1) by POWER:25; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: S₁[n + 1]

then n - 1 in NAT by INT_1:5, NAT_1:14;
then reconsider m = n - 1 as Nat ;
A3: 2 <= 2 to_power (m + 1) by LMC31B;
A2: 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27
.= (2 to_power n) * 2 by POWER:25
.= (2 to_power n) + (2 to_power n) ;
(2 * n) + 2 <= (2 to_power n) + (2 to_power n) by A3, XREAL_1:7, A1;
hence 2 * (n + 1) <= 2 to_power (n + 1) by A2; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
hence for k being Nat holds 2 * k <= 2 to_power k ; :: thesis: verum