proposition: Lemma mem_orbit x : {homo f : y / y \in orbit x}.
proof: Proof. by move=> y; rewrite -!fconnect_orbit => /connect_trans->//; apply: fconnect1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)