proposition: Lemma psupport_restr_perm X s : X \in porbit_set s -> psupport (restr_perm X s) = X.
proof: Proof. Proof using. move => HX; apply/eqP; rewrite eqEsubset psupport_restr_perm_incl /=. apply/subsetP => y Hin; rewrite in_psupport. rewrite restr_permE ?porbit_set_astabs // -in_psupport. rewrite -(cover_partition (partition_psupport s)). by apply/bigcupP; 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