proposition: Lemma permcycles_inj s : 'injm (permcycles s).
proof: Proof. Proof using. apply/injmP; apply: can_in_inj; exact: permcyclesK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype