proposition: Lemma size_row_extract t U V : is_tableau t -> V \in (tabcols t) -> sorted <=%O (extract (in_tuple (to_word t)) U) -> #|U :&: V| <= 1.
proof: Proof. Proof using. move=> Htab HV Hleq. have: U :&: V \subset U by apply/subsetP => j; rewrite !inE=> /andP[]. move/(extsubsI (in_tuple (to_word t)))/(subseq_sorted le_trans). move/(_ Hleq) => {}Hleq. have Htmp := sorted_gt_tabcols Htab. have := HV; rewrite -index_mem => {}/Htmp. rewrite (nth_index _ HV) => Hgtn. have: U :&: V \subset V by apply/subsetP => j; rewrite !inE=> /andP[]. move/(extsubsI (in_tuple (to_word t)))/(subseq_sorted gt_trans). move/(_ Hgtn) => {}Hgtn. rewrite -(size_extract (in_tuple (to_word t))). case: (extract _ _) Hleq Hgtn => [// | l0 [// | l1 s]] /=. by move=> /andP[]; rewrite ltNge => -> /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype