proposition: Lemma partition_cent_rcoset (H : {group gT}) g (C := 'C_H[g]) (Cg := C :* g) : g \in 'N(H) -> coprime #|H| #[g] -> partition (Cg :^: H) (H :* g) /\ #|Cg :^: H| = #|H : C|.
proof: Proof. move=> nHg coHg; pose pi := \pi(#[g]). have notCg0: Cg != set0 by apply/set0Pn; exists g; apply: rcoset_refl. have id_pi: {in Cg, forall u, u.`_ pi = g}. move=> _ /rcosetP[u /setIP[Hu cgu] ->]; rewrite consttM; last exact/cent1P. rewrite (constt_p_elt (pgroup_pi _)) (constt1P _) ?mul1g //. by rewrite (mem_p_elt _ Hu) // /pgroup -coprime_pi' // coprime_sym. have{id_pi} /and3P[_ tiCg /eqP defC]: normedTI Cg H C. apply/normedTI_P; rewrite subsetI subsetIl normsM ?normG ?subsetIr //. split=> // x Hx /pred0Pn[u /andP[/= Cu Cxu]]; rewrite !inE Hx /= conjg_set1. by rewrite -{2}(id_pi _ Cu) -(conjgKV x u) consttJ id_pi -?mem_conjg. have{tiCg} partCg := partition_class_support notCg0 tiCg. have{defC} oCgH: #|Cg :^: H| = #|H : C| by rewrite -defC -astab1Js -card_orbit. split=> //; congr (partition _ _): (partCg); apply/eqP. rewrite eqEcard card_rcoset {1}class_supportEr; apply/andP; split. apply/bigcupsP=> x Hx; rewrite conjsgE -rcosetM conjgCV rcosetM mulgA. by rewrite mulSg ?mul_subG ?subsetIl // sub1set ?memJ_norm ?groupV. have oCg Cx: Cx \in Cg :^: H -> #|Cx| = #|C|. by case/imsetP=> x _ ->; rewrite cardJg card_rcoset. by rewrite (card_uniform_partition oCg partCg) oCgH mulnC Lagrange ?subsetIl. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)