proposition: Lemma trivg_max_norm P : 1%G \in |/|*(P; pi) -> |/|*(P; pi) = [set 1%G].
proof: Proof. move=> max1; apply/eqP; rewrite eqEsubset sub1set max1 andbT. apply/subsetP=> Q; rewrite !inE -val_eqE /= in max1 *. by case/maxgroupP: max1 => _ max1; move/maxgroupp; move/max1->; rewrite ?sub1G. 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)