proposition: Lemma in_orbit_cycle : {in p &, forall x, orbit x =i p}.
proof: Proof. by move=> x y xp yp; rewrite (orbitE fcycle_undup)// ?mem_rot ?mem_undup. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)