proposition: Lemma fcycle_consE : x :: p = traject f x (size p).+1.
proof: Proof. by have := fcycle_rconsE; rewrite trajectSr => /rcons_inj[/= <-]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)