proposition: Lemma injectivePcycle x : reflect {in orbit x &, injective f} (fcycle f (orbit x)).
proof: Proof. apply: (iffP idP) => [/inj_cycle//|/cycle_orbit_in]. by apply; [apply: mem_orbit|apply: in_orbit]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)