simp [hp]
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.sub (p ^ 2) 0 ≠ 0
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ ¬p = 0