proposition: Lemma posbinSF : posb \in S = false.
proof: Proof. Proof using HS HbNin. apply/negP => Hb. by move: HbNin; rewrite /cover => /bigcupP[]; exists S. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene