exact Nat.Coprime.mul_right h1 h2
p1 q1 p2 q2 : ℕ
hp1 : p1.Prime
hq1 : q1.Prime
hp2 : p2.Prime
hq2 : q2.Prime
hp1q1 : p1 ≠ q1
hp1q2 : p1 ≠ q2
hp2q1 : p2 ≠ q1
hp2q2 : p2 ≠ q2
h1 : (p1 * p2).Coprime q1
h2 : (p1 * p2).Coprime q2
⊢ (p1 * p2).Coprime (q1 * q2)
no goals