proposition: Lemma ST_cover_disjoint : [disjoint S :|: T & cover (P :\: [set S; T])].
proof: Proof. Proof using HS HT Px. rewrite -setI_eq0; apply/eqP/setP => i; rewrite in_set0. apply/negP; move: Px => /and3P[_ /trivIsetP Htriv _]. rewrite !inE => /andP[] /orP[] Hi /bigcupP[U]; rewrite !inE negb_or => /andP[/andP[HUS HUT] HU] HiU. - move/(_ _ _ HU HS HUS): Htriv; rewrite -setI_eq0 => /eqP. by apply/setP => /(_ i); rewrite in_set0 !inE Hi HiU. - move/(_ _ _ HU HT HUT): Htriv; rewrite -setI_eq0 => /eqP. by apply/setP => /(_ i); rewrite in_set0 !inE Hi HiU. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene