proposition: Lemma max_pgroupJ pi M G x : x \in G -> [max M | pi.-subgroup(G) M] -> [max M :^ x of M | pi.-subgroup(G) M].
proof: Proof. move=> Gx /maxgroupP[piM maxM]; apply/maxgroupP. split=> [|H piH]; first by rewrite psubgroupJ. by rewrite -(conjsgKV x H) conjSg => /maxM/=-> //; rewrite psubgroupJ ?groupV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)