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