case cons =>
  rcases h with (rfl | h); { exact Or.inl (Nat.lt_succ_self _) }
  exact Or.inr (ih h)
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
no goals