exact Nat.Coprime.mul_right h1 (ih hy)
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x * xs.prod)
no goals