for m, n being Nat st m < n holds
ex p being Element of NAT st
( n = m + p & 1 <= p )