for p, q, n being Nat st n > 0 holds
( (p - q) mod n = 0 iff p mod n = q mod n )