exact Nat.lt_trans h.left (Nat.lt_succ_self _)
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1
no goals