proposition: Lemma partition_class_support A G : A != set0 -> trivIset (A :^: G) -> partition (A :^: G) (class_support A G).
proof: Proof. rewrite /partition cover_imset -class_supportEr eqxx => nzA ->. by apply: contra nzA => /imsetP[x _ /eqP]; rewrite eq_sym -!cards_eq0 cardJg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)