have h2 : Nat.Coprime p2 q := Iff.mpr (Nat.coprime_primes hp2 hq) hp2q
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
⊢ (p1 * p2).Coprime q
p1 p2 q : ℕ
hp1 : p1.Prime
hp2 : p2.Prime
hq : q.Prime
hp1q : p1 ≠ q
hp2q : p2 ≠ q
h1 : p1.Coprime q
h2 : p2.Coprime q
⊢ (p1 * p2).Coprime q