by_contra nlt
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
⊢ s.count < n
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
⊢ False