proposition: Lemma tabrows_non0 t : is_part (shape t) -> forall s, s \in tabrows t -> s != set0.
proof: Proof. Proof using. move=> Hpart S'. rewrite /tabrows => /mapP[S HS -> {S'}]. rewrite -card_gt0 card_imset; last exact: cast_ord_inj. pose crd := (fun S : {set 'I_(sumn (shape t))} => #|S|). have: crd S \in map crd (shrows (shape t)) by apply/mapP; exists S. rewrite {}/crd /= shrows_cards. move: (#|S|) => i {S HS}. elim: t Hpart i => [//= | t0 t IHt] Hpart i /=. rewrite inE => /orP[/eqP -> |]. - by move: Hpart => /part_head_non0 /=; case: (size t0). - by apply: IHt; exact: (is_part_consK Hpart). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype