proposition: Lemma iter_findex x y : fconnect f x y -> iter (findex x y) f x = y.
proof: Proof. rewrite [_ y]fconnect_orbit => fxy; pose i := index y (orbit x). have lt_ix: i < order x by rewrite -size_orbit index_mem. by rewrite -(nth_traject f lt_ix) nth_index. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)