Definition. divisors_eq
divisors a = {d | d ∈ ℕ ∧ divides d a}