proposition: Lemma permcyclesP P : (permcycles P) \in 'C[s].
proof: Proof. Proof using. apply/cent1P; exact: permcyclesC. 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