rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ h with x_lt_n | x_eq_n
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
⊢ (Array.range (n + 1))[x] = x
case inl
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_lt_n : x < n
⊢ (Array.range (n + 1))[x] = x

case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x