proposition: Lemma image_orbit x : {subset image f (orbit x) <= orbit x}.
proof: Proof. by move=> _ /mapP[y yin ->]; apply: mem_orbit; rewrite ?mem_enum in yin. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)