proposition: Lemma disjointS1T1 : [disjoint S1 & T1].
proof: Proof. Proof using HRabc HS HT Hposa Hposb Px. rewrite -setI_eq0; apply/eqP/setP => i; rewrite in_set0. apply/negP; rewrite /S1 /T1 !inE => /andP[]. have:= TS_disjoint => /disjoint_setI0/setP => Hdisj. move=> /orP[] /andP[Hi1 /= H1] /orP[] /andP[Hi2 /= H2]. - by move/(_ i): Hdisj; rewrite inE Hi1 Hi2 in_set0. - by have:= leq_trans H2 H1; rewrite ltnn. - have Hu2 := ltn_trans (ltnSn (size u)) (ltnSn _). by have:= leq_ltn_trans H2 (ltn_trans Hu2 H1); rewrite ltnn. - by move/(_ i): Hdisj; rewrite inE Hi1 Hi2 in_set0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene