proposition: Lemma stab_iporbits_homog P : {in porbits s, forall C : {set T}, #|(if P \in stab_iporbits s then P else 1) C| = #|C| }.
proof: Proof. Proof using. case: (boolP (_ \in _)) => [|_]. - rewrite inE => /andP[_ /bigcapP /= HP] C HC; rewrite /inporbits /=. have:= subsetT C => /subset_leqif_cards []; rewrite -ltnS cardsT => cardC _. move/(_ (Ordinal cardC) isT): HP => /= /astabsP/(_ C). by rewrite !inE HC eq_refl /= => /andP[_ /eqP]. - by move=> C _; rewrite perm1. 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