proposition: Lemma abelian_type_dprod_homocyclic p K H G : K \x H = G -> p.-group G -> homocyclic G -> abelian_type K = nseq 'r(K) (exponent G) /\ abelian_type H = nseq 'r(H) (exponent G).
proof: Proof. move=> defG pG homG; have [cGG _] := andP homG. have /mulG_sub[sKG sHG]: K * H = G by case/dprodP: defG. have [cKK cHH] := (abelianS sKG cGG, abelianS sHG cGG). suffices: all (pred1 (exponent G)) (abelian_type K ++ abelian_type H). rewrite all_cat => /andP[/all_pred1P-> /all_pred1P->]. by rewrite !size_abelian_type. suffices def_atG: abelian_type K ++ abelian_type H =i abelian_type G. rewrite (eq_all_r def_atG); apply/all_pred1P. by rewrite size_abelian_type // -abelian_type_homocyclic. have [bK defK atK] := abelian_structure cKK. have [bH defH atH] := abelian_structure cHH. apply/perm_mem; rewrite perm_sym -atK -atH -map_cat. apply: (abelian_type_pgroup pG); first by rewrite big_cat defK defH. have: all [pred m | m > 1] (map order (bK ++ bH)). by rewrite map_cat all_cat atK atH !abelian_type_gt1. by rewrite all_map (eq_all (@order_gt1 _)) all_predC has_pred1. 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)