proposition: Theorem irrSGP : perm_eq [seq 'irrSG[la] | la : 'P_n] (irr 'SG_n).
proof: Proof. set IRR := [seq 'irrSG[la] | la : 'P_n]. have Huniq : uniq IRR. rewrite map_inj_uniq ?enum_uniq // => la mu Hlamu. apply/eqP; have:= irrSG_orthonormal la mu. rewrite Hlamu irrSG_orthonormal eq_refl /=. by case: eqP => //= _ /eqP; rewrite oner_eq0. apply (uniq_perm Huniq). exact: (free_uniq (basis_free (irr_basis _))). have /(uniq_min_size Huniq) Htmp : {subset IRR <= irr 'SG_n}. move=> /= f /mapP[/= p /mapP[/= la _ ->{p}] ->{f}]. exact: irrSG_irr. suff /Htmp [] : (size (irr 'SG_n) <= size IRR)%N by []. rewrite size_tuple -(vector.size_basis (irr_basis _)) dim_cfun. rewrite card_classes_perm /=. by rewrite size_tuple card_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama