let i, j be Nat; :: thesis: ( i <= j implies ex k being Nat st j = i + k )
defpred S1[ Nat] means ( i <= $1 implies ex k being Nat st $1 = i + k );
A1: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A2: ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: S1[j + 1]
assume A3: i <= j + 1 ; :: thesis: ex k being Nat st j + 1 = i + k
per cases ( i <= j or i = j + 1 ) by A3, NAT_1:8;
suppose i <= j ; :: thesis: ex k being Nat st j + 1 = i + k
then consider k being Nat such that
A4: j = i + k by A2;
reconsider k1 = k + 1 as Nat ;
take k1 ; :: thesis: j + 1 = i + k1
thus j + 1 = i + k1 by A4; :: thesis: verum
end;
suppose B1: i = j + 1 ; :: thesis: ex k being Nat st j + 1 = i + k
reconsider k1 = 0 as Nat ;
take k1 ; :: thesis: j + 1 = i + k1
thus j + 1 = i + k1 by B1; :: thesis: verum
end;
end;
end;
A6: S1[ 0 ]
proof
assume A7: i <= 0 ; :: thesis: ex k being Nat st 0 = i + k
take 0 ; :: thesis: 0 = i + 0
thus 0 = i + 0 by A7; :: thesis: verum
end;
for j being Nat holds S1[j] from NAT_1:sch 2(A6, A1);
 hence ( i <= j implies ex k being Nat st j = i + k ) ; :: thesis: verum