proposition: Lemma trajectP x n y : reflect (exists2 i, i < n & y = iter i f x) (y \in traject f x n).
proof: Proof. elim: n x => [|n IHn] x /=; first by right; case. rewrite inE; have [-> | /= neq_xy] := eqP; first by left; exists 0. apply: {IHn}(iffP (IHn _)) => [[i] | [[|i]]] // lt_i_n ->. by exists i.+1; rewrite ?iterSr. by exists i; rewrite ?iterSr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)