refine' ⟨p, _, pp⟩
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ p > n