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