proposition: Lemma rcons_rcons w a b : rcons (rcons w a) b = w ++ [:: a; b].
proof: Proof. Proof using. by rewrite -!cats1 -catA cat1s. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr