proposition: Lemma quotient_maximal_eq : K <| G -> K <| H -> maximal_eq (G / K) (H / K) = maximal_eq G H.
proof: Proof. by move=> nKG nKH; rewrite -cosetpre_maximal_eq ?quotientGK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)