rw [heq]
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬i ≤ ↑k
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