for a, b, c being Nat st 0 < a & 0 < b & a < c & b < c & c is prime holds
(a * b) mod c <> 0