obtain ⟨k', hk'⟩ := exists_eq_mul_right_of_dvd (Nat.dvd_of_mod_eq_zero hm)
a n : ℕ
ha : 0 < a
hm : a % n = 0
⊢ ∃ k, a = n * ↑k
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
⊢ ∃ k, a = n * ↑k