proposition: Lemma hyper_stdtabP sh : is_stdtab (hyper_stdtab sh).
proof: Proof. Proof using . by rewrite /hyper_stdtab /= RSstdE std_is_std. 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