proposition: Lemma fcycle_rconsE : rcons (x :: p) x = traject f x (size p).+2.
proof: Proof. by rewrite rcons_cons; have /fpathE-> := f_p; rewrite size_rcons. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)