proposition: Lemma cover_bin : cover Qbin = cover P.
proof: Proof. Proof using HRabc HS HT Hposa Hposb Hposc Px. have:= coverS1T1; rewrite /Qbin /cover !bigcup_setU => ->. apply/setP/subset_eqP/andP; split; apply/subsetP=> i. - rewrite !inE => /orP[]; first move=> /orP[]. + by move=> Hi; apply/bigcupP; exists S. + by move=> Hi; apply/bigcupP; exists T. + move/bigcupP => [U]; rewrite inE => /andP[_ HU Hi]. by apply/bigcupP; exists U. - move/bigcupP => [U HU Hi]; rewrite !inE. case/altP: (U =P S) => HUS; last case/altP: (U =P T) => HUT. + by subst U; rewrite Hi. + by subst U; rewrite Hi orbT. + apply/orP; right; apply/bigcupP. exists U; last exact Hi. by rewrite !inE negb_or HUS HUT HU. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene