proposition: Lemma trivIset_iporbits s : trivIset [set porbits s :&: 'SC_i | i : 'I_#|T|.+1].
proof: Proof. Proof using. apply/trivIsetP => A B /imsetP[i _ ->{A}] /imsetP[j _ ->{B}] Hij. have {}Hij : i != j by move: Hij; apply contra => /eqP -> . rewrite -setI_eq0; apply/eqP/setP => x. rewrite !inE -!andbA; apply/negP => /and4P[_ /eqP -> _] /eqP /val_inj Hieqj. by rewrite Hieqj eq_refl in Hij. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype