proposition: Lemma max_normed_uniq A P Q : |/|*(A; pi) = [set Q] -> A \subset P -> P \subset 'N(Q) -> |/|*(P; pi) = [set Q].
proof: Proof. move=> defAmax sAP nQP; have: Q \in |/|*(A; pi) by rewrite defAmax set11. rewrite inE; case/maxgroupP; case/andP=> piQ _ maxQ. apply/setP=> X; rewrite !inE -val_eqE /=; apply/maxgroupP/eqP=> [[]|->{X}]. case/andP=> piX nXP maxX; have nXA := subset_trans sAP nXP. have [Y] := max_normed_exists piX nXA. by rewrite defAmax; move/set1P->; move/maxX=> -> //; rewrite piQ. rewrite piQ; split=> // X; case/andP=> piX nXP sQX. by rewrite (maxQ X) // piX (subset_trans sAP). Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)