let m, n be Nat; ( n < m implies ex k being Nat st m = (n + 1) + k )
assume A1:
n < m
; ex k being Nat st m = (n + 1) + k
then consider k1 being Nat such that
A2:
m = n + k1
by NAT_1:10;
k1 <> 0
by A1, A2;
then consider n1 being Nat such that
A3:
k1 = n1 + 1
by NAT_1:6;
take
n1
; m = (n + 1) + n1
thus
m = (n + 1) + n1
by A2, A3; verum