rw [dif_neg h]
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = d