rewrite [Nat.succ_add] at h
case h.h.h.h.succ
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n k : Nat
h : succ m + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f (succ m) (_ : succ m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
case h.h.h.h.succ
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
init : α
n k : Nat
h✝ : succ m + n = k
h : succ (m + n) = k
f : Fin k → α → α
⊢ fold'TR.loop k f (succ m) (_ : succ m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init