proposition: Lemma ksupp0 k : set0 \is a k.-supp.
proof: Proof. Proof using. rewrite unfold_in cards0 leq0n /=; apply/andP; split. - by apply/trivIsetP => A B; rewrite in_set0. - by apply/forallP => A; rewrite in_set0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype