proposition: Lemma abelian_disjoint_psupports A : disjoint_psupports A -> abelian <<A>>.
proof: Proof. Proof using. move=> [] /trivIsetP Htriv Hinj. rewrite abelian_gen abelianE; apply/subsetP => /= C HC. apply/centP => D HD. case: (C =P D) => [-> // | HCD]. apply psupport_disjointC. apply Htriv; try exact: imset_f. by apply/contra_notN: HCD => /eqP/Hinj; apply. 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