theorem Th18: :: REAL_3:18

for a, b, n, m being Nat st a < b & (modSeq (m,n)) . a = 0 holds
(divSeq (m,n)) . b = 0