let n, m be Nat; :: thesis: for k being Element of NAT st k <> 0 & k + m <= n holds
m < n
let k be Element of NAT ; :: thesis: ( k <> 0 & k + m <= n implies m < n )
assume A1: k <> 0 ; :: thesis: ( not k + m <= n or m < n )
assume A2: k + m <= n ; :: thesis: m < n

per cases ( k + m < n or k + m = n ) by A2, XXREAL_0:1;

suppose k + m < n ; :: thesis: m < n

hence m < n by NAT_1:12; :: thesis: verum

end;

suppose A3: k + m = n ; :: thesis: m < n

assume not m < n ; :: thesis: contradiction
then m + k >= n + k by XREAL_1:7;
then n - n >= (n + k) - n by A3, XREAL_1:9;
hence contradiction by A1; :: thesis: verum

end;

end;