proposition: Lemma maxnormal_normal A B : maxnormal A B B -> A <| B.
proof: Proof. by case/maxsetP=> /and3P[/gen_set_id /= -> pAB nAB]; rewrite /normal proper_sub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)