proposition: Lemma loopingP x n : reflect (forall m, iter m f x \in traject f x n) (looping x n).
proof: Proof. apply: (iffP idP) => loop_n; last exact: loop_n. case: n => // n in loop_n *; elim=> [|m /= IHm]; first exact: mem_head. move: (fpath_traject x n) loop_n; rewrite /looping !iterS -last_traject /=. move: (iter m f x) IHm => y /splitPl[p1 p2 def_y]. rewrite cat_path last_cat def_y; case: p2 => // z p2 /and3P[_ /eqP-> _] _. by rewrite inE mem_cat mem_head !orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)