proposition: Lemma card_subcent1_coset G H x : x \in G -> H <| G -> (#|'C_(G / H)[coset H x]| <= #|'C_G[x]|)%N.
proof: Proof. move=> Gx nsHG; rewrite -leC_nat. move: (second_orthogonality_relation x Gx); rewrite mulrb class_refl => <-. have GHx: coset H x \in (G / H)%g by apply: mem_quotient. move: (second_orthogonality_relation (coset H x) GHx). rewrite mulrb class_refl => <-. rewrite -2!(eq_bigr _ (fun _ _ => normCK _)) sum_norm_irr_quo // -subr_ge0. rewrite (bigID (fun i => H \subset cfker 'chi[G]_i)) //= addrC addKr. by apply: sumr_ge0 => i _; rewrite normCK mul_conjC_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)