theorem LmN: :: NEWTON07:69

for n, k being Nat st k in Seg (n + 1) holds
ex l, m being Nat st
( l = k - 1 & m = n - l )