proposition: Lemma abelian_perm_dec S s : trivIset S -> abelian <<perm_dec S s>>.
proof: Proof. Proof using. by move=> /disjoint_perm_dec Htriv; apply abelian_disjoint_psupports. 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