theorem :: NAT_1:17

for m being Nat st 0 < m holds
for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m )