let m, n be Nat; :: thesis: ( m < n implies ex k being Nat st
( m + k = n & k > 0 ) )
assume A1: m < n ; :: thesis: ex k being Nat st
( m + k = n & k > 0 )
then consider k being Nat such that
A2: m + k = n by NAT_1:10;
m - m < n - m by A1, XREAL_1:16;
hence ex k being Nat st
( m + k = n & k > 0 ) by A2; :: thesis: verum