Transitivity of iterated function application

Iterated applications of a function compose across step counts (Function.iterate_trans).

Main results

• Function.iterate_trans: if f^[m] a = b and f^[n] b = c, then f^[n + m] a = c.

theorem Function.iterate_trans {α : Type u_1} {f : α → α} {a b c : α} {m n : ℕ} (h₁ : f^[m] a = b) (h₂ : f^[n] b = c) : f^[n + m] a = c

Iterated function applications compose across step counts.