proposition: Lemma findex_iter x i : i < order x -> findex x (iter i f x) = i.
proof: Proof. move=> lt_ix; rewrite -(nth_traject f lt_ix) /findex index_uniq ?orbit_uniq //. by rewrite size_orbit. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)