Nat.Coprime.eq_one_of_dvd takes Coprime k n and k ∣ n (not a third divisor)

Nat.Coprime.eq_one_of_dvd : Nat.Coprime k n → k ∣ n → k = 1. To show a divisor q of n with Coprime n q is 1, you need Nat.Coprime.eq_one_of_dvd (Nat.coprime_comm.1 h) hqn. To kill a common factor 3 ∣ n, 3 ∣ m with Coprime n m, use Nat.Coprime.eq_one_of_dvd (Nat.Coprime.coprime_dvd_left h3n hcop) h3m, which gives 3 = 1. Related renames: Nat.prime_def_lt'' is gone, use Nat.prime_def_lt' (2 ≤ p ∧ ∀ m, 2 ≤ m → m < p → ¬m ∣ p). Odd.of_dvd_nat lives in Mathlib.Algebra.Order.Ring.Abs. Nat.eq_two_pow_or_exists_odd_prime_and_dvd (Data.Nat.Factors) is the right split for 'n is a power of 2' conclusions.