proposition: Lemma mul_card_Ohm_Mho_abelian n G : abelian G -> (#|'Ohm_n(G)| * #|'Mho^n(G)|)%N = #|G|.
proof: Proof. case/abelian_structure => b defG _. elim: b G defG => [_ <-|x b IHb G]. by rewrite !big_nil (trivgP (Ohm_sub _ _)) (trivgP (Mho_sub _ _)) !cards1. rewrite big_cons => defG; rewrite -(dprod_card defG). rewrite -(dprod_card (Ohm_dprod n defG)) -(dprod_card (Mho_dprod n defG)) /=. rewrite mulnCA -!mulnA mulnCA mulnA; case/dprodP: defG => [[_ H _ defH] _ _ _]. rewrite defH {b G defH IHb}(IHb H defH); congr (_ * _)%N => {H}. have [m] := ubnP #[x]; elim: m x => // m IHm x /ltnSE-lexm. case p_x: (p_group <[x]>); last first. case: (eqVneq x 1) p_x => [-> |]; first by rewrite cycle1 p_group1. rewrite -order_gt1 /p_group -orderE; set p := pdiv _ => ntx p'x. have def_x: <[x.`_p]> \x <[x.`_p^']> = <[x]>. have ?: coprime #[x.`_p] #[x.`_p^'] by rewrite !order_constt coprime_partC. have ?: commute x.`_p x.`_p^' by apply: commuteX2. rewrite dprodE ?coprime_TIg -?cycleM ?consttC //. by rewrite cent_cycle cycle_subG; apply/cent1P. rewrite -(dprod_card (Ohm_dprod n def_x)) -(dprod_card (Mho_dprod n def_x)). rewrite mulnCA -mulnA mulnCA mulnA. rewrite !{}IHm ?(dprod_card def_x) ?(leq_trans _ lexm) {m lexm}//. rewrite /order -(dprod_card def_x) -!orderE !order_constt ltn_Pmull //. rewrite p_part -(expn0 p) ltn_exp2l 1?lognE ?prime_gt1 ?pdiv_prime //. by rewrite order_gt0 pdiv_dvd. rewrite proper_card // properEneq cycle_subG mem_cycle andbT. by apply: contra (negbT p'x); move/eqP <-; apply: p_elt_constt. case/p_groupP: p_x => p p_pr p_x. rewrite (Ohm_p_cycle n p_x) (Mho_p_cycle n p_x) -!orderE. set k := logn p #[x]; have ox: #[x] = (p ^ k)%N by rewrite -card_pgroup. case: (leqP k n) => [le_k_n | lt_n_k]. rewrite -(subnKC le_k_n) subnDA subnn expg1 expnD expgM -ox. by rewrite expg_order expg1n order1 muln1. rewrite !orderXgcd ox -[in (p ^ k)%N](subnKC (ltnW lt_n_k)) expnD. rewrite gcdnC gcdnMl gcdnC gcdnMr. by rewrite mulnK ?mulKn ?expn_gt0 ?prime_gt0. 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)