proposition: Lemma tabcol_cut t : is_part (shape t) -> forall B, \sum_(U <- tabcols t) #|B :&: U| = #|B|.
proof: Proof. Proof using. move=> Hpart /= B. rewrite (_ : \sum_(U <- _) _ = \sum_(U <- [seq B :&: U | U <- tabcols t]) #|U|); last by rewrite big_map. have Htriv := @trivIseq_tabcols _ _ t. have : trivIseq [seq B :&: U | U <- tabcols t]. rewrite /trivIseq => i j; rewrite size_map => Hijs. have:= Hijs => /andP[Hij Hj]. have Hi := ltn_trans Hij Hj. rewrite -setI_eq0 (nth_map set0 _ _ Hi) (nth_map set0 _ _ Hj). rewrite setIACA setIid. move: Hijs => /Htriv; rewrite -setI_eq0 => /eqP ->. by rewrite setI0. move/trivIseq_cover ->; congr #|_|. rewrite big_map. rewrite (_ : \bigcup_(j <- _) _ = B :&: (\bigcup_(j <- tabcols t) j)); first last. apply: esym; apply: big_morph; last by rewrite setI0. by move=> i j /=; rewrite setIUr. by rewrite bigcup_seq_cover (cover_tabcols Hpart) setIT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype