proposition: Lemma fconnect_findex x y : fconnect f x y -> y != x -> findex x y = (findex (f x) y).+1.
proof: Proof. rewrite /findex fconnect_orbit /orbit -orderSpred /= inE => /orP [-> //|]. rewrite eq_sym; move=> yin /negPf->; have [_ eq_o|_ ->//] := orderPcycle x. by rewrite -(orderSpred (f x)) trajectSr -cats1 index_cat -eq_o yin. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)