proposition: Lemma disjoint_cover (A B : {set 'I_N}) : [disjoint cover P & cover Q] -> A \in P -> B \in Q -> [disjoint A & B].
proof: Proof. Proof using. rewrite -!setI_eq0 => /eqP; rewrite -setP => Hcov HA HB. apply/eqP/setP => i; rewrite in_set0. apply/idP/idP; move/(_ i): Hcov; rewrite !inE /cover => /negbT. apply contra => /andP[HiA HiB]. by apply/andP; split; apply/bigcupP; [exists A | exists B]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene