proposition: Lemma p_rank_p'quotient G H : (p : nat)^'.-group H -> G \subset 'N(H) -> 'r_p(G / H) = 'r_p(G).
proof: Proof. move=> p'H nHG; have [P sylP] := Sylow_exists p G. have [sPG pP _] := and3P sylP; have nHP := subset_trans sPG nHG. have tiHP: H :&: P = 1 := coprime_TIg (p'nat_coprime p'H pP). rewrite -(p_rank_Sylow sylP) -(p_rank_Sylow (quotient_pHall nHP sylP)). by rewrite (isog_p_rank (quotient_isog nHP tiHP)). 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)