proposition: Lemma yamtab_rcons sh sn : yamtab (rcons sh sn) = rcons (yamtab sh) (nseq sn (size sh)).
proof: Proof. rewrite /yamtab -[size sh]addn0. move: (0) => i. elim: sh i => [//= | s0 sh IHsh] /= i . by rewrite IHsh addSnnS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple finfun finset path bigop order) tools partition Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact