proposition: Lemma partition_porbits s : partition (porbits s) setT.
proof: Proof. Proof using. rewrite /porbits porbitE. have /orbit_partition : [acts <[s]>, on [set: T] | 'P]. by apply/actsP => x _ t; rewrite !inE. congr partition; apply/setP => x. by apply/imsetP/imsetP => [] [y _ Hy]; 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