proposition: Lemma inporbits1 s t : t \in 'C(porbits s | ('P)^* ) -> inporbits s t = 1.
proof: Proof. Proof using. move=> Ht; have tfix := astab_act Ht. apply/permP => /= X; rewrite /inporbits perm1. case: (boolP (X \in porbits s)) => HX. - rewrite restr_permE //= ?actpermE ?tfix // {X HX}. apply/astabsP => X /=; rewrite actpermK. by apply astabs_act; move: Ht; apply/subsetP; exact: astab_sub. - exact: (out_perm (restr_perm_on _ _ ) 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