proposition: Lemma permcyclesC P : commute (permcycles P) s.
proof: Proof. Proof using. by apply esym; apply/permP => x; rewrite !permM !permE; exact: cymapP. 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