for a, b, n, m being Nat holds
( not a < b or (modSeq (m,n)) . a > (modSeq (m,n)) . b or (modSeq (m,n)) . a = 0 )