apply isCoprime_of_prime_dvd
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
case nonzero
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ ¬(3 ^ 2 * 2 * s = 0 ∧ q ^ 2 + 3 * s ^ 2 = 0)

case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ ∀ (z : ℤ), Prime z → z ∣ 3 ^ 2 * 2 * s → ¬z ∣ q ^ 2 + 3 * s ^ 2