proposition: Lemma disjoint_psupport_subset (S1 S2 : {set {perm T}}) : S1 \subset S2 -> disjoint_psupports S2 -> disjoint_psupports S1.
proof: Proof. Proof using. rewrite /disjoint_psupports => Hsubs [Htriv Hinj]. split. - exact: (trivIsetS (imsetS _ Hsubs) Htriv). - move/subsetP in Hsubs. by move=> s t /Hsubs Hs /Hsubs; exact: Hinj. 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