proposition: Lemma fcycle_consEflatten : exists k, x :: p = flatten (nseq k.+1 (orbit x)).
proof: Proof. move: f_p; rewrite fcycle_consE; elim/ltn_ind: (size p) => n IHn t_cycle. have := order_le_cycle t_cycle (mem_head _ _); rewrite size_traject. case: ltngtP => [||<-] //; last by exists 0; rewrite /= cats0. rewrite ltnS => n_ge _; have := t_cycle. rewrite -(subnKC n_ge) -addnS trajectD. rewrite (iter_order_in (mem_fcycle f_p) (inj_cycle f_p)) ?mem_head//. set m := (_ - _) => cycle_cat. have [||k->] := IHn m; last by exists k.+1. by rewrite ltn_subrL (leq_trans _ n_ge) ?order_gt0. move: cycle_cat; rewrite -orderSpred/= rcons_cat rcons_cons -cat_rcons. by rewrite cat_path last_rcons => /andP[]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)