fact: Fixpoint shuffle u v {struct u} := if u is a :: u' then shuffle_from_rec a u' (shuffle u') v else [:: v].
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