apply Nat.not_le_of_gt
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬n ≤ ↑k
case h
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ n > ↑k