let m, n be Nat; :: thesis: ( n < m implies ex k being Nat st m = (n + 1) + k )
assume A1: n < m ; :: thesis: 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 ; :: thesis: m = (n + 1) + n1
thus m = (n + 1) + n1 by A2, A3; :: thesis: verum