proposition: Lemma normedTI_P A G L : reflect [/\ A != set0, L \subset 'N_G(A) & {in G, forall g, ~~ [disjoint A & A :^ g] -> g \in L}] (normedTI A G L).
proof: Proof. apply: (iffP and3P) => [[nzA /trivIsetP tiAG /eqP <-] | [nzA sLN tiAG]]. split=> // g Gg; rewrite inE Gg (sameP normP eqP) /= eq_sym; apply: contraR. by apply: tiAG; rewrite ?mem_orbit ?orbit_refl. have [/set0Pn[a Aa] /subsetIP[_ nAL]] := (nzA, sLN); split=> //; last first. rewrite eqEsubset sLN andbT; apply/subsetP=> x /setIP[Gx nAx]. by apply/tiAG/pred0Pn=> //; exists a; rewrite /= (normP nAx) Aa. apply/trivIsetP=> _ _ /imsetP[x Gx ->] /imsetP[y Gy ->]; apply: contraR. rewrite -setI_eq0 -(mulgKV x y) conjsgM; set g := (y * x^-1)%g. have Gg: g \in G by rewrite groupMl ?groupV. rewrite -conjIg (inj_eq (act_inj 'Js x)) (eq_sym A) (sameP eqP normP). by rewrite -cards_eq0 cardJg cards_eq0 setI_eq0 => /tiAG/(subsetP nAL)->. 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)