rwa [← Ideal.isCoprime_span_singleton_iff,
  ← Ideal.span_singleton_eq_span_singleton.mpr (associated_zeta_sub_one_pow_prime hζ),
  ← Ideal.span_singleton_pow, IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd,
  hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff, Ideal.dvd_span_singleton,
  Ideal.mem_span_singleton]
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ IsCoprime (↑↑p) x
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
hx : ¬↑hζ.unit' - 1 ∣ x
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ 0 < ↑p - 1