m k n : ℕ+
⊢ ↑m ∣ ↑k → Coprime k n → Coprime m n
m k n : ℕ+
⊢ m ∣ k → Coprime k n → Coprime m n
rw [dvd_iff]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
m k n : ℕ+
⊢ ↑m ∣ ↑k → Coprime k n → Coprime m n
repeat' rw [← coprime_coe]
no goals
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
apply Nat.coprime.coprime_dvd_left
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
rw [← coprime_coe]