∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K] {r s t w : NumberField.RingOfIntegers K},
  ¬hζ.toInteger - 1 ∣ r →
    ¬hζ.toInteger - 1 ∣ s →
      (∀ {p : NumberField.RingOfIntegers K}, Prime p → p ∣ t → p ∣ w → Associated p (hζ.toInteger - 1)) →
        (∀ {q : NumberField.RingOfIntegers K}, q ∣ r → q ∣ t) →
          (∀ {q : NumberField.RingOfIntegers K}, q ∣ s → q ∣ w) → IsCoprime r s