proposition: Lemma findex_max x y : fconnect f x y -> findex x y < order x.
proof: Proof. by rewrite [_ y]fconnect_orbit -index_mem size_orbit. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)