proposition: Lemma coverS1T1 : cover [set S1; T1] = (S :|: T).
proof: Proof. Proof using HRabc HS HT Hposa Hposb Hposc Px. rewrite /cover bigcup_setU !big_set1. apply/setP/subset_eqP/andP; split; apply/subsetP=> i; rewrite !inE. - by move/or3P => [/orP[] | | ] /andP[-> _] //=; rewrite orbT. - move/orP => [] Hi; rewrite Hi /=. + by case: (ltnP (size u).+1 i); first rewrite !orbT. + case: (leqP i (size u)) => Hiu; first by rewrite orbT. rewrite /=; apply/orP; left; apply/orP; right. have:= TS_disjoint => /disjoint_setI0/setP => Hdisj. case: (ltnP (size u).+2 i) => //= Hi2. case: (ltnP (size u).+1 i) => Hi1. * have Htmp : i = posc. by apply: val_inj => /=; apply/eqP; rewrite eqn_leq Hi2 Hi1. subst i => {Hi1 Hi2 Hiu}. by move/(_ posc): Hdisj; rewrite in_set0 in_setI Hi Hposc. * have Htmp : i = posa. by apply: val_inj => /=; apply/eqP; rewrite eqn_leq Hiu Hi1. subst i => {Hi1 Hi2 Hiu}. by move/(_ posa): Hdisj; rewrite in_set0 in_setI Hi Hposa. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene