proposition: Lemma all_in_shuffler u v : predI (mem u) (mem v) =i pred0 -> all (fun s => filter (mem v) s == v) (shuffle u v).
proof: Proof. Proof using . move=> HI. rewrite (perm_all _ (shuffleC _ _)) //. apply: all_in_shufflel. by move=> i; rewrite -(HI i) !inE andbC. 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