proposition: Lemma set_gring_classM_coef (i j k : 'I_#|classes G|) g : g \in enum_val k -> a i j k = #|gring_classM_coef_set (enum_val i) (enum_val j) g|.
proof: Proof. rewrite /a; have /repr_classesP[] := enum_valP k; move: (repr _) => g1 Gg1 ->. have [/imsetP[zi Gzi ->] /imsetP[zj Gzj ->]] := (enum_valP i, enum_valP j). move=> g1Gg; have Gg := subsetP (class_subG Gg1 (subxx _)) _ g1Gg. set Aij := gring_classM_coef_set _ _. without loss suffices IH: g g1 Gg Gg1 g1Gg / (#|Aij g1| <= #|Aij g|)%N. by apply/eqP; rewrite eqn_leq !IH // class_sym. have [w Gw Dg] := imsetP g1Gg; pose J2 (v : gT) xy := (xy.1 ^ v, xy.2 ^ v)%g. have J2inj: injective (J2 w). by apply: can_inj (J2 w^-1)%g _ => [[x y]]; rewrite /J2 /= !conjgK. rewrite -(card_imset _ J2inj) subset_leq_card //; apply/subsetP. move=> _ /imsetP[[x y] /setIdP[/andP[/= x1Gx y1Gy] Dxy1] ->] /[!inE]/=. rewrite !(class_sym _ (_ ^ _)) !classGidl // class_sym x1Gx class_sym y1Gy. by rewrite -conjMg (eqP Dxy1) /= -Dg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)