proposition: Lemma partition_psupport s : partition (porbit_set s) (psupport s).
proof: Proof. Proof using. rewrite /porbit_set /porbits porbitE. have /orbit_partition : [acts <[s]>, on psupport s | 'P]. apply/actsP => t /cycleP[i -> {t}] x; rewrite !in_psupport /=. rewrite -permM -expgSr expgS permM; congr negb. by apply/eqP/eqP => [/perm_inj| ->]. congr partition; apply/setP => x. rewrite !inE; apply/imsetP/andP => [[y Hy -> {x}] | [/imsetP[y _ -> {x}]]]. - split; first exact: imset_f. by rewrite -porbitE psupport_card_porbit. - rewrite -porbitE psupport_card_porbit => Hy. by exists y. 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