proposition: Lemma all_size_shuffle u v : all (fun s => size s == size u + size v) (shuffle u v).
proof: Proof. Proof using . apply/allP => x Hx; rewrite -size_cat. apply/eqP; apply: perm_size. have:= perm_shuffle u v => /allP Hall. by rewrite perm_sym; exact: Hall. 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