proposition: Lemma mem_shuffle u v s : predI (mem u) (mem v) =i pred0 -> [&& filter (mem u) s == u, filter (mem v) s == v & (size s == size u + size v)] = (s \in shuffle u v).
proof: Proof. Proof using . move=> HI; apply/idP/idP. - move=> /and3P[/eqP Hu /eqP Hv /eqP Hsz]. exact: (mem_shuffle_pred HI). - move=> Hs. have:= all_in_shufflel HI => /allP/(_ _ Hs) -> /=. have:= all_in_shuffler HI => /allP/(_ _ Hs) -> /=. by have:= all_size_shuffle u v => /allP/(_ _ Hs). 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