proposition: Lemma allLeq_is_row_rcons w b : allLeq w b -> forall row, row \in RS w -> is_row (rcons row b).
proof: Proof. Proof using. move=> H row Hin; apply: is_row_rcons. - move: Hin; have:= is_tableau_RS w. elim: (RS w) => [// | t0 t IHt] /= /and4P[_ Hrow _ Htab]. rewrite inE => /orP[]. + by move/eqP => ->. + exact: IHt. - have: allLeq (to_word (RS w)) b by rewrite (perm_allLeq (perm_RS w)). elim: (RS w) Hin => [// | t0 t IHt] /=. rewrite inE to_word_cons => /orP[/eqP ->|]. + rewrite allLeq_catE => /andP[_]; case/lastP: t0 => [// | t0 tn]. by move/allLeq_last; rewrite last_rcons. + by move=> Hrow; rewrite allLeq_catE => /andP[/(IHt Hrow)]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr