proposition: Lemma orbit_prefix n x : n <= order f x -> orbit f x = traject f x n ++ drop n (orbit f x).
proof: Proof. move => le_n_ox. by rewrite /orbit -(subnKC le_n_ox) trajectD drop_size_cat // size_traject. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)