proposition: Lemma fcycle_undup : fcycle f (undup p).
proof: Proof. case: p f_p => [//|x q] f_q; rewrite undup_cycle_cons//. by rewrite (cycle_orbit_in (mem_fcycle f_q) (inj_cycle f_q)) ?mem_head. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)