proposition: Lemma arc_orbit (x y : T) : fconnect f x y -> arc (orbit f x) x y = traject f x (findex f x y).
proof: Proof. move=> conn_xy; rewrite /arc index_orbit rot0 /findex; set i := index y _. suff I : i <= order f x by rewrite -(take_traject _ _ I). by apply: ltnW; rewrite -size_orbit index_mem -fconnect_orbit. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)