proposition: Lemma orderPcycle x : order_spec_cycle x (fcycle f (orbit x)).
proof: Proof. have [xcycle|Ncycle] := boolP (fcycle f (orbit x)); constructor => //. by rewrite order_id_cycle. rewrite /order (eq_card (_ : _ =1 [predU1 x & fconnect f (f x)])). by rewrite cardU1 inE (contraNN (all_iffLR orbitPcycle 2 0)). by move=> y; rewrite !inE fconnect_eqVf eq_sym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)