theorem :: FINSEQ_4:84

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