theorem Th15: :: REAL_3:15

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 )