proposition: Lemma porbit_set_eq0 s : (s == perm_one T) = (porbit_set s == set0).
proof: Proof. Proof using. rewrite -subset0 /porbit_set; apply/eqP/subsetP => [-> C| H]. - rewrite !inE => /andP[/imsetP[x _ ->]]. by rewrite psupport_card_porbit in_psupport permE eq_refl. - apply/permP => x; rewrite permE; apply/eqP. have:= H (porbit s x); rewrite !inE imset_f //= => /contraT. by apply contraLR; rewrite -in_psupport psupport_card_porbit. 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