proposition: Lemma card_support_normedTI A G L : normedTI A G L -> #|class_support A G| = (#|A| * #|G : L|)%N.
proof: Proof. case/and3P=> ntA tiAG /eqP <-; rewrite -card_conjugates mulnC. apply: card_uniform_partition (partition_class_support ntA tiAG). by move=> _ /imsetP[y _ ->]; rewrite 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)