proposition: Lemma Ohm_Mho_homocyclic (n p : nat) G : abelian G -> p.-group G -> 0 < n < logn p (exponent G) -> 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G) -> homocyclic G.
proof: Proof. set e := exponent G => cGG pG /andP[n_gt0 n_lte] eq_Ohm_Mho. suffices: all (pred1 e) (abelian_type G). by rewrite /homocyclic cGG; apply: all_pred1_constant. case/abelian_structure: cGG (abelian_type_gt1 G) => b defG <-. set H := G in defG eq_Ohm_Mho *; have sHG: H \subset G by []. elim: b H defG sHG eq_Ohm_Mho => //= x b IHb H. rewrite big_cons => defG; case/dprodP: defG (defG) => [[_ K _ defK]]. rewrite defK => defHm cxK; rewrite setIC => /trivgP-tiKx defHd. rewrite -{}[in H \subset G]defHm mulG_subG cycle_subG ltnNge -trivg_card_le1. case/andP=> Gx sKG; rewrite -(Mho_dprod _ defHd) => /esym defMho /andP[ntx ntb]. have{defHd} defOhm := Ohm_dprod n defHd. apply/andP; split; last first. apply: (IHb K) => //; have:= dprod_modr defMho (Mho_sub _ _). rewrite -(dprod_modr defOhm (Ohm_sub _ _)). rewrite !(trivgP (subset_trans (setIS _ _) tiKx)) ?Ohm_sub ?Mho_sub //. by rewrite !dprod1g. have:= dprod_modl defMho (Mho_sub _ _). rewrite -(dprod_modl defOhm (Ohm_sub _ _)) . rewrite !(trivgP (subset_trans (setSI _ _) tiKx)) ?Ohm_sub ?Mho_sub //. move/eqP; rewrite eqEcard => /andP[_]. have p_x: p.-elt x := mem_p_elt pG Gx. have [p_pr p_dv_x _] := pgroup_pdiv p_x ntx. rewrite !dprodg1 (Ohm_p_cycle _ p_x) (Mho_p_cycle _ p_x) -!orderE. rewrite orderXdiv ?leq_divLR ?pfactor_dvdn ?leq_subr //. rewrite orderXgcd divn_mulAC ?dvdn_gcdl // leq_divRL ?gcdn_gt0 ?order_gt0 //. rewrite leq_pmul2l //; apply: contraLR. rewrite eqn_dvd dvdn_exponent //= -ltnNge => lt_x_e. rewrite (leq_trans (ltn_Pmull (prime_gt1 p_pr) _)) ?expn_gt0 ?prime_gt0 //. rewrite -expnS dvdn_leq // ?gcdn_gt0 ?order_gt0 // dvdn_gcd. rewrite pfactor_dvdn // dvdn_exp2l. by rewrite -[ltnRHS]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x. rewrite ltn_sub2r // ltnNge -(dvdn_Pexp2l _ _ (prime_gt1 p_pr)) -!p_part. by rewrite !part_pnat_id // (pnat_dvd (exponent_dvdn G)). 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)