proposition: Lemma disjoint_perm_dec S s : trivIset S -> disjoint_psupports (perm_dec S s).
proof: Proof. Proof using. move=> Htriv. have Hinj : {in perm_dec S s &, injective psupport}. move => C1 C2 /imsetP[c1 Hc1 ->] /imsetP[c2 HC2 ->] H. by rewrite -(restr_perm_psupportE c1 s) H restr_perm_psupportE. split; last exact: Hinj. apply/trivIsetP. move=> C1 C2 /imsetP[c1 /imsetP[S1 HS1 -> ->]]. move=> /imsetP[c2 /imsetP[S2 HS2 -> ->]] Hs12. rewrite -setI_eq0 -subset0; apply/subsetP => x. rewrite inE in_set0 => /andP[]. move=> /(subsetP (psupport_restr_perm_incl _ _)) => HxS1. move=> /(subsetP (psupport_restr_perm_incl _ _)) => HxS2. move: Htriv => /trivIsetP/(_ S1 S2 HS1 HS2) H. have {}/H : S1 != S2 by apply/contra: Hs12 => /eqP ->. rewrite -setI_eq0 => /eqP/setP/(_ x). by rewrite !inE HxS1 HxS2. 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