proposition: Lemma p2Elem_dprodP p A E X Y : E \in 'E_p^2(A) -> X \in 'E_p^1(E) -> Y \in 'E_p^1(E) -> reflect (X \x Y = E) (X :!=: Y).
proof: Proof. move=> Ep2E EpX EpY; have [_ abelE oE] := pnElemPcard Ep2E. apply: (iffP (TIp1ElemP EpX EpY)) => [tiXY|]; last by case/dprodP. have [[sXE _ oX] [sYE _ oY]] := (pnElemPcard EpX, pnElemPcard EpY). rewrite dprodE ?(sub_abelian_cent2 (abelem_abelian abelE)) //. by apply/eqP; rewrite eqEcard mul_subG //= TI_cardMg // oX oY oE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)