proposition: Lemma cover_iporbits s : cover [set porbits s :&: 'SC_i | i : 'I_#|T|.+1] = porbits s.
proof: Proof. Proof using. apply/setP => C; apply/bigcupP/idP => [[/= X] | Hx]. - by move=> /imsetP[/= i _ ->{X}]; rewrite inE => /andP[]. - have:= subsetT C => /subset_leqif_cards []; rewrite -ltnS cardsT => cardC _. exists (porbits s :&: 'SC_(Ordinal cardC)); first exact: imset_f. by rewrite !inE Hx /=. 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