fact: Definition ksupp (k : nat) := [qualify a P : {set {set 'I_N}} | [&& (#|P| <= k)%N, trivIset P & [forall (s | s \in P), sorted R (extract s)]]].
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype