proposition: Lemma fconnect_orbit x y : fconnect f x y = (y \in orbit x).
proof: Proof. apply/idP/idP=> [/connectP[_ /fpathP[m ->] ->] | /trajectP[i _ ->]]. by rewrite last_traject; apply/loopingP/looping_order. exact: fconnect_iter. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)