n : ℕ
⊢ ((fun b => comp succ b)^[n]) zero = Code.const n
n : ℕ
⊢ ((fun b => comp succ (n, b).snd)^[id n]) zero = Code.const n
simp
no goals
n : ℕ
⊢ ((fun b => comp succ b)^[n]) zero = Code.const n
induction n <;>
simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]