proposition: Lemma orbitPcycle {x} : [<-> fcycle f (orbit x); order (f x) = order x; x \in fconnect f (f x); exists k, iter k.+1 f x = x; iter (order x) f x = x; {in orbit x &, injective f}].
proof: Proof. tfae=> [xorbit_cycle|||[k fkx]|fx y z|/injectivePcycle//]. - by apply: eq_order_cycle xorbit_cycle _ _ _ _; rewrite ?mem_orbit. - move=> /subset_cardP/(_ _)->; rewrite ?inE//; apply/subsetP=> y. by apply: connect_trans; apply: fconnect1. - by exists (findex (f x) x); rewrite // iterSr iter_findex. - apply: (@iter_order_cycle (traject f x k.+1)); rewrite /= ?mem_head//. by apply/fpathP; exists k.+1; rewrite trajectSr -iterSr fkx. - rewrite -!fconnect_orbit => /iter_findex <- /iter_findex <-. move/(congr1 (iter (order x).-1 f)). by rewrite -!iterSr !orderSpred -!iterD ![order _ + _]addnC !iterD fx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)