exact Nat.Prime.not_dvd_one hp h_p_div_one
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
h_p_div_one : p ∣ 1
⊢ False
no goals