no goals
α : Type u_1
l : List α
i : Nat
h : i < length l
⊢ i + (length l - 1 - i) + 1 = length l
rw [Nat.add_sub_of_le (Nat.le_pred_of_lt h),
  Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]