theorem :: NAT_1:18

for n, m, k, t, k1, t1 being natural Number st n = (m * k) + t & t < m & n = (m * k1) + t1 & t1 < m holds
( k = k1 & t = t1 )