People,
the Standard lib-0.7 defines
data _∣_ : ℕ → ℕ → Set where
divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n
Why does not it use the existing library constructor of `∃' by defining
_∣_ : Rel ℕ Level.zero
m ∣ n = ∃ \ q → (q * m ≡ n)
?
Thanks,
------
Sergei