suffices ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α), fold'TR.loop k f m (h ▸ m.le_add_right n) (fold' n (fun i => f ⟨i.1, trans i.2 (h ▸ n.le_add_left m)⟩) init) = fold' k f init
from (this n 0 _ rfl f).symm
case h.h.h.h
α : Type u_1
n : Nat
f : Fin n → α → α
init : α
⊢ fold' n f init = fold'TR n f init
case h.h.h.h
α : Type u_1
n : Nat
f : Fin n → α → α
init : α
⊢ ∀ (m 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