proposition: Lemma size_shuffle u v : size (shuffle u v) = binomial ((size u) + (size v)) (size u).
proof: Proof. Proof using . elim: u v => [| a u IHu] /= v; first by rewrite bin0. elim: v => [| b v IHv] /=; first by rewrite addn0 binn. rewrite size_cat !size_map IHu IHv /=. by rewrite !addSn addnS addnC -binS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype finfun fintype choice) mathcomp(order seq tuple finset perm binomial bigop) tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab Schensted plactic Greene_inv stdplact