let k be Nat; :: thesis: for n being Nat st k <= n holds
n + k <= 2 to_power n
defpred S₁[ Nat] means ($1 + k) + k <= 2 to_power ($1 + k);
2 * k <= 2 to_power k by LMC31D;
then 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]
A2: 2 to_power (k + (n + 1)) = 2 to_power ((k + n) + 1)
.= (2 to_power (k + n)) * (2 to_power 1) by POWER:27
.= (2 to_power (k + n)) * 2 by POWER:25
.= (2 to_power (k + n)) + (2 to_power (k + n)) ;
1 <= 2 to_power (k + n)

proof

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

suppose k + n = 0 ; :: thesis: 1 <= 2 to_power (k + n)

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

end;

suppose k + n <> 0 ; :: thesis: 1 <= 2 to_power (k + n)

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

end;

end;

end;

then ((n + k) + k) + 1 <= (2 to_power (k + n)) + (2 to_power (k + n)) by XREAL_1:7, A1;
hence ((n + 1) + k) + k <= 2 to_power ((n + 1) + k) by A2; :: thesis: verum

end;

X1: for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
let n be Nat; :: thesis: ( k <= n implies n + k <= 2 to_power n )
assume k <= n ; :: thesis: n + k <= 2 to_power n
then n - k in NAT by INT_1:5;
then reconsider m = n - k as Nat ;
(m + k) + k <= 2 to_power (m + k) by X1;
hence n + k <= 2 to_power n ; :: thesis: verum