proposition: Lemma partn_exponentS pi H G : H \subset G -> #|G|`_pi %| #|H| -> (exponent H)`_pi = (exponent G)`_pi.
proof: Proof. move=> sHG Gpi_dvd_H; apply/eqP; rewrite eqn_dvd. rewrite partn_dvd ?exponentS ?exponent_gt0 //=; apply/dvdn_partP=> // p. rewrite pi_of_part ?exponent_gt0 // => /andP[_ /= pi_p]. have sppi: {subset (p : nat_pred) <= pi} by move=> q /eqnP->. have [P sylP] := Sylow_exists p H; have sPH := pHall_sub sylP. have{} sylP: p.-Sylow(G) P. rewrite pHallE (subset_trans sPH) //= (card_Hall sylP) eqn_dvd andbC. by rewrite -{1}(partn_part _ sppi) !partn_dvd ?cardSg ?cardG_gt0. rewrite partn_part ?partn_biglcm //. apply: (@big_ind _ (dvdn^~ _)) => [|m n|x Gx]; first exact: dvd1n. by rewrite dvdn_lcm => ->. rewrite -order_constt; have p_y := p_elt_constt p x; set y := x.`_p in p_y *. have sYG: <[y]> \subset G by rewrite cycle_subG groupX. have [z _ Pyz] := Sylow_Jsub sylP sYG p_y. rewrite (bigD1 (y ^ z)) ?(subsetP sPH) -?cycle_subG ?cycleJ //=. by rewrite orderJ part_pnat_id ?dvdn_lcml // (pi_pnat p_y). 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)