no goals
α : Type u_1
f : Nat → α → α
n✝ : Nat
init : α
n : Nat
⊢ foldTR.loop f (0 + n) 0 (fold f n init) = fold f (0 + n) init
simp [foldTR.loop]
α : Type u_1
f : Nat → α → α
n✝ : Nat
init : α
m n : Nat
⊢ foldTR.loop f (succ (m + n)) m (f n (fold f n init)) = fold f (succ (m + n)) init
α : Type u_1
f : Nat → α → α
n✝ : Nat
init : α
m n : Nat
⊢ foldTR.loop f (succ m + n) (succ m) (fold f n init) = fold f (succ m + n) init
rw [foldTR.loop, add_sub_self_left, succ_add]
no goals
α : Type u_1
f : Nat → α → α
n✝ : Nat
init : α
m n : Nat
⊢ foldTR.loop f (succ (m + n)) m (f n (fold f n init)) = fold f (succ (m + n)) init
exact go m (succ n)