proposition: Lemma cent1_normedTI A G L : normedTI A G L -> {in A, forall x, 'C_G[x] \subset L}.
proof: Proof. case/normedTI_memJ_P=> [_ _ tiAG] x Ax; apply/subsetP=> y /setIP[Gy cxy]. by rewrite -(tiAG x) // /(x ^ y) -(cent1P cxy) mulKg. 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)