proposition: Lemma shape_hyper_stdtabnP d (P : 'P_d) : shape (hyper_stdtabn P) = P.
proof: Proof. Proof using . rewrite shape_RS_std (shape_RS_yam (hyper_yamP (intpartnP P))). by rewrite (evalseq_hyper_yam (intpartnP P)). 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