proposition: Lemma posb_inSF : (posb \in S) = false.
proof: Proof. Proof using HRabc HS HT Hposa Hposb Px. have:= TS_disjoint; rewrite -setI_eq0 => /eqP/setP/(_ posb). by rewrite in_set0 !inE Hposb andbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene