proposition: Lemma perm_decE S s : trivIset S -> psupport s \subset cover S -> s \in 'C(S | ('P)^* ) -> \prod_(C in perm_dec S s) C = s.
proof: Proof. Proof using. move=> Htriv /subsetP Hcover Hact. apply/permP => x. case: (boolP (x \in psupport s)) => Hx; first last. rewrite out_perm_prod. + by move: Hx; rewrite in_psupport negbK => /eqP ->. + move=> Ctmp /imsetP[C HC ->{Ctmp}]. move: Hx; apply contra; rewrite !in_psupport => H. by have:= H; rewrite (restr_perm_neq H). have:= Hcover x Hx => /bigcupP[C HC HxC]. have Hrestr : (restr_perm (T:=T) C s) x = s x. rewrite restr_permE // -astab1_set. move: Hact => /astab_act/(_ HC) Hact. by apply/astabP => D; rewrite inE => /eqP ->{D}. rewrite (prod_of_disjoint (C := restr_perm C s)). - exact: Hrestr. - exact: disjoint_perm_dec. - exact: imset_f. - by move: Hx; rewrite !in_psupport Hrestr. 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