proposition: Lemma sizeIk k : #|Ik k| = minn N k.
proof: Proof. Proof using. rewrite !cardE size_filter. rewrite (eq_count (a2 := (gtn k) \o val)); last by move=> i /=; rewrite in_set. rewrite -count_map /enum_mem -enumT /= val_enum_ord. by rewrite -size_filter iotagtnk size_iota. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype