k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * m * l
⊢ m ∣ n
k m n : Nat
kpos : 0 < k
H : k * m ∣ k * n
⊢ m ∣ n
let ⟨l, H⟩ := H
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * (m * l)
⊢ m ∣ n
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * m * l
⊢ m ∣ n
rw [Nat.mul_assoc] at H
no goals
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * (m * l)
⊢ m ∣ n
exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩