nat.coprime_of_dvd

Stream: general

[Ruben Van de Velde]

We currently have

theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, 1 < k → k ∣ m → ¬ k ∣ n) : coprime m n := sorry
theorem coprime_of_dvd' {m n : ℕ} (H : ∀ k, k ∣ m → k ∣ n → k ∣ 1) : coprime m n := sorry

but I found the following forms easier to use:

theorem coprime_of_dvd_prime {m n : ℕ} (H : ∀ k, prime k → k ∣ m → ¬ k ∣ n) : coprime m n := sorry
theorem coprime_of_dvd'_prime {m n : ℕ} (H : ∀ k, prime k → k ∣ m → k ∣ n → k ∣ 1) : coprime m n := sorry

Should I add those? Or replace the originals?

[Anne Baanen]

If you can easily prove the second set without using the first, I would vote in favour of replacing. Otherwise adding them sounds good.

[Ruben Van de Velde]

The first proof got somewhat longer, but that's mostly because I couldn't figure out how to do it all in term mode

[Ruben Van de Velde]

I'll try to take a look later if adapting any of the current uses is painful