calc
_ ≤ Nat.succ i + j' := Nat.le_add_right _ _
_ = n := hj
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' i : ℕ
hj✝ : i + (j' + 1) = n
hj : i.succ + j' = n
acc : α
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
⊢ i < n
no goals