simp
case h.e'_4
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
⊢ 1 = (n + 1).factorial + 1 - (n + 1).factorial
no goals