proposition: Lemma freeSchurP Q (t : d.-tuple 'I_n) : t \in freeSchur Q = (val t \in langQ Q).
proof: Proof. Proof using . by rewrite /freeSchur /langQ !inE /=. 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