proposition: Lemma maximal_eqP M G : reflect (M \subset G /\ forall H, M \subset H -> H \subset G -> H :=: M \/ H :=: G) (maximal_eq M G).
proof: Proof. rewrite subEproper /maximal_eq; case: eqP => [->|_]; first left. by split=> // H sGH sHG; right; apply/eqP; rewrite eqEsubset sHG. apply: (iffP maxgroupP) => [] [sMG maxM]; split=> // H. by move/maxM=> maxMH; rewrite subEproper; case/predU1P; auto. by rewrite properEneq => /andP[/eqP neHG sHG] /maxM[]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)