proposition: Lemma size_cover_tabcolsk k t : is_part (shape t) -> #|cover [set s | s \in (tabcolsk t k)]| = \sum_(l <- (shape t)) minn l k.
proof: Proof. Proof using. elim: t => [| t0 t IHt] /=; first by rewrite cover_nil big_nil. move/andP => [Hhead {}/IHt IHt]. have {}Hhead : head 0 (shape t) <= size t0. apply: (@leq_trans (head 1 (shape t))); last exact Hhead. by case t. rewrite big_cons -IHt {IHt} /=. have:= cover_tabcols_rec k Hhead; rewrite /tabcols /=. set s := (X in X = _); set sl := (X in _ = X :|: _); set sr := (X in _ = _ :|: X). move/(congr1 (fun s : {set _} => #|s|)); rewrite cardsU. have /disjoint_setI0 -> : [disjoint sl & sr]. rewrite /sl /sr {sl sr s} !imset_comp /disjoint /=. apply/pred0P => l /=; apply/negP => /andP[]. move=> /imsetP[l1 Hl1 {l} ->] /imsetP[l Hl /cast_ord_inj H]; subst l1. move: Hl Hl1 => /imsetP[l1 Hl1 {l} ->] /imsetP[l Hl /eqP]. by rewrite eq_lrshift. rewrite cards0 subn0 /s {s} => ->. have -> : #|sl| = minn (size t0) k. rewrite /sl imset_comp card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: rshift_inj. by rewrite sizeIk. apply/eqP; rewrite eqn_add2l {sl} /sr. rewrite imset_comp card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: lshift_inj. by rewrite -map_take. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype