proposition: Lemma trivIset_Qbin : trivIset Qbin.
proof: Proof. Proof using HRabc HS HT Hposa Hposb Hposc Px. apply: trivIset_coverU. - apply/trivIsetP => A B; rewrite !inE => /orP[] /eqP -> /orP[] /eqP -> //=. + by rewrite eq_refl. + by move=> _; exact: disjointS1T1. + by move=> _; rewrite disjoint_sym; exact: disjointS1T1. + by rewrite eq_refl. - apply: (@trivIsetS _ _ P); first exact: subsetDl. by move: Px => /and3P[_]. - by rewrite coverS1T1; apply: ST_cover_disjoint. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene