let k, n be Nat; :: thesis: ( k <> 0 implies n < n + k )
assume k <> 0 ; :: thesis: n < n + k
then A1: n <> n + k ;
( n <= n + k & n <= k + n ) by Th12;
hence n < n + k by A1, XXREAL_0:1; :: thesis: verum