proposition: Lemma nth_traject i n : i < n -> forall x, nth x (traject x n) i = iter i f x.
proof: Proof. elim: n => // n IHn; rewrite ltnS => le_i_n x. rewrite trajectSr nth_rcons size_traject. by case: ltngtP le_i_n => [? _||->] //; apply: IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)