have := Nat.le_of_dvd zero_lt_one this
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
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
this : p ≤ 1
⊢ False