proposition: Lemma normedTI_memJ_P A G L : reflect [/\ A != set0, L \subset G & {in A & G, forall a g, (a ^ g \in A) = (g \in L)}] (normedTI A G L).
proof: Proof. apply: (iffP normedTI_P) => [[-> /subsetIP[sLG nAL] tiAG] | [-> sLG tiAG]]. split=> // a g Aa Gg; apply/idP/idP=> [Aag | Lg]; last first. by rewrite memJ_norm ?(subsetP nAL). by apply/tiAG/pred0Pn=> //; exists (a ^ g)%g; rewrite /= Aag memJ_conjg. split=> // [ | g Gg /pred0Pn[ag /=]]; last first. by rewrite andbC => /andP[/imsetP[a Aa ->]]; rewrite tiAG. apply/subsetP=> g Lg; have Gg := subsetP sLG g Lg. by rewrite !inE Gg; apply/subsetP=> _ /imsetP[a Aa ->]; rewrite tiAG. 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)