let k be Nat; :: thesis: for n being Nat st k <= n holds
n + k <= 2 to_power n
defpred S1[ Nat] means ($1 + k) + k <= 2 to_power ($1 + k);
2 * k <= 2 to_power k by LMC31D;
then P1: S1[ 0 ] ;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A1: S1[n] ; :: thesis: S1[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 S1[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