proposition: Lemma p_rank_dprod K H G : K \x H = G -> 'r_p(K) + 'r_p(H) = 'r_p(G).
proof: Proof. move=> defG; apply/eqP; rewrite eqn_leq -leq_subLR andbC. have [_ defKH cKH tiKH] := dprodP defG; have nKH := cents_norm cKH. rewrite {1}(isog_p_rank (quotient_isog nKH tiKH)) /= -quotientMidl defKH. rewrite p_rank_quotient; last by rewrite -defKH mul_subG ?normG. have [[E EpE] [F EpF]] := (p_rank_witness p K, p_rank_witness p H). have [[sEK abelE <-] [sFH abelF <-]] := (pnElemP EpE, pnElemP EpF). have defEF: E \x F = E <*> F. by rewrite dprodEY ?(centSS sFH sEK) //; apply/trivgP; rewrite -tiKH setISS. apply/p_rank_geP; exists (E <*> F)%G; rewrite !inE (dprod_abelem p defEF). rewrite -lognM ?cargG_gt0 // (dprod_card defEF) abelE abelF eqxx. by rewrite -(genGid G) -defKH genM_join genS ?setUSS. 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)