proposition: Lemma hyper_stdtabnP d (P : 'P_d) : is_stdtab_of_n d (hyper_stdtab P).
proof: Proof. Proof using . rewrite /is_stdtab_of_n /= hyper_stdtabP /= size_RS. rewrite size_std -evalseq_eq_size (evalseq_hyper_yam (intpartnP P)). by rewrite sumn_intpartn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly