proposition: Lemma cprod_extraspecial G H K : p.-group G -> H \* K = G -> H :&: K = 'Z(H) -> extraspecial H -> extraspecial K -> extraspecial G.
proof: Proof. move=> pG defG ziHK [[PhiH defH'] ZH_pr] [[PhiK defK'] ZK_pr]. have [_ defHK cHK]:= cprodP defG. have sZHK: 'Z(H) \subset 'Z(K). by rewrite subsetI -{1}ziHK subsetIr subIset // centsC cHK. have{sZHK} defZH: 'Z(H) = 'Z(K). by apply/eqP; rewrite eqEcard sZHK leq_eqVlt eq_sym -dvdn_prime2 ?cardSg. have defZ: 'Z(G) = 'Z(K). by case/cprodP: (center_cprod defG) => /= _ <- _; rewrite defZH mulGid. split; first split; rewrite defZ //. by have /cprodP[_ <- _] := Phi_cprod pG defG; rewrite PhiH PhiK defZH mulGid. by have /cprodP[_ <- _] := der_cprod 1 defG; rewrite defH' defK' defZH mulGid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)