have : p ∣ Nat.factorial (n + 1) := by
  apply Nat.dvd_factorial
  apply pp.pos
  linarith
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ False
case intro.intro
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ False