k m n : Nat
kpos : 0 < k
H : k * m ∣ k * n
⊢ m ∣ n
k m n : Nat
kpos : 0 < k
H : m * k ∣ n * k
⊢ m ∣ n
rw [Nat.mul_comm m k, Nat.mul_comm n k] at H
no goals
k m n : Nat
kpos : 0 < k
H : k * m ∣ k * n
⊢ m ∣ n
exact Nat.dvd_of_mul_dvd_mul_left kpos H