proposition: Lemma size_cover_tabrows k t : is_part (shape t) -> #|cover [set s | s \in (tabrowsk t k)]| = sumn (take k (shape t)).
proof: Proof. Proof using. move=> Hpart. have:= trivIset_tabrowsk k t; rewrite /trivIset /= => /eqP <-. rewrite /cover bigop_trivIseq; first last. - apply: (trivIsubseq (v := tabrows t)); first exact: subseq_take. rewrite /tabrows; apply: trivIseq_map; first exact: cast_ord_inj. exact: trivIseq_shrows. - by apply/allP => S /mem_take HS; exact: tabrows_non0. elim: t k {Hpart} => [// | t0 t IHt] /= k; first by rewrite !big_nil. case: k => [// | k]; first by rewrite !big_nil. move/(_ k): IHt; rewrite /= big_cons => <-. rewrite /sym_cast imset_comp card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: rshift_inj. rewrite card_ord; congr (_ + _). rewrite /tabrows -!map_take /shiftset /=. move: (take _ _) => S. elim: S => [| s0 S IHS] /=; first by rewrite !big_nil. rewrite !big_cons. rewrite /sym_cast imset_comp card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: lshift_inj. rewrite card_imset; last exact: cast_ord_inj. by congr (_ + _); exact: IHS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype