have : p ∣ 1 := by
  convert Nat.dvd_sub' pdvd this
  simp
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
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
this : p ∣ 1
⊢ False