proposition: Lemma psupport_cycle_dec s : [set psupport C | C in cycle_dec s] = porbit_set s.
proof: Proof. Proof using. apply/setP => X; apply/imsetP/idP. - move => [x /imsetP[x0 Hx0 ->] ->]. by rewrite psupport_restr_perm. - rewrite inE => /andP[HX1 HX2]. have HX: X \in porbit_set s by rewrite inE HX1 HX2. exists (restr_perm X s); last by rewrite psupport_restr_perm. by apply/imsetP; exists X. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp