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