by_contra ple
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ p > n
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : ¬p > n
⊢ False