Definition. prime_equi
prime a ↔ 2 ≤ a ∧ divisors a = {1, a}