proposition: Lemma partition_normedTI A G L : normedTI A G L -> partition (A :^: G) (class_support A G).
proof: Proof. by case/and3P=> ntA tiAG _; apply: partition_class_support. 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)