proposition: Lemma posaT1_bin : posb \in T1.
proof: Proof. Proof using Hposb. by rewrite /T1 !inE Hposb leqnn. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene