Definition. divides_equi
divides m a ↔ ∃k. k ∈ ℤ ∧ a = m⋅k