proposition: Lemma TS_disjoint : [disjoint S & T].
proof: Proof. Proof using HRabc HS HT Hposa Hposb Px. move: Px => /and3P[_ /trivIsetP Hdisj _]. by move/(_ _ _ HT HS TSneq): Hdisj; rewrite disjoint_sym. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene