proposition: Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}.
proof: Proof. move=> x xS; rewrite /orbit -orderSpred (cycle_path x) /= last_traject. by rewrite -/(finv x) fpath_traject f_finv_in ?eqxx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)