proposition: Lemma injm_maximal : maximal (f @* M) (f @* G) = maximal M G.
proof: Proof. rewrite -(morphpre_invm injf) -(morphpre_invm injf G). by rewrite morphpre_maximal ?morphim_invm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)