proposition: Lemma cfRepr_inj n1 n2 rG1 rG2 : @cfRepr _ G n1 rG1 = @cfRepr _ G n2 rG2 -> mx_rsim rG1 rG2.
proof: Proof. move=> eq_repr12; pose c i : algC := (standard_irr_coef _ (W i))%:R. have [rsim1 rsim2] := (mx_rsim_standard rG1, mx_rsim_standard rG2). apply: mx_rsim_trans (rsim1) (mx_rsim_sym _). suffices ->: standard_grepr rG1 = standard_grepr rG2 by []. apply: eq_bigr => Wi _; congr (muln_grepr _ _); apply/eqP; rewrite -eqC_nat. rewrite -[Wi]irr_of_socleK -!/(c _ _ _) -!(coord_sum_free (c _ _) _ irr_free). rewrite -!eq_sum_nth_irr -!cfRepr_standard. by rewrite -(cfRepr_sim rsim1) -(cfRepr_sim rsim2) eq_repr12. 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)