proposition: Lemma mmax_sup_id M : M \in 'M -> 'M(M) = [set M].
proof: Proof. move=> maxM; apply/eqP; rewrite eqEsubset sub1set inE maxM subxx !andbT. apply/subsetP=> H; case/setIdP=> maxH; rewrite inE -val_eqE /=. by move/eq_mmax=> ->. 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)