have hkp : 0 < k' := lt_of_mul_lt_mul_left' (hk' ▸ ha)
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
⊢ ∃ k, a = n * ↑k
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
hkp : 0 < k'
⊢ ∃ k, a = n * ↑k