proposition: Lemma fcycleEflatten : exists k, p = flatten (nseq k (undup p)).
proof: Proof. case: p f_p => [//|x q] f_q; first by exists 0. have [k {1}->] := @fcycle_consEflatten x q f_q. by exists k.+1; rewrite undup_cycle_cons. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)