for a, n, m being Nat st (divSeq (m,n)) . (a + 1) = 0 holds
(modSeq (m,n)) . a = 0