proposition: Lemma porbit_permcycles P x : P \in stab_iporbits s -> porbit s (permcycles P x) = P (porbit s x).
proof: Proof. Proof using. by rewrite permE porbit_cymap /= => ->. 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