proposition: Lemma mem_shuffle_predU u v s Pu Pv: predI Pu Pv =i pred0 -> filter Pu s = u -> filter Pv s = v -> size s = size u + size v -> filter (predU Pu Pv) s = s.
proof: Proof. Proof using . move=> HI Hu Hv Hsz. have /eqP := count_predUI Pu Pv s. rewrite -!size_filter Hu Hv (eq_filter HI) filter_pred0 /= addn0 -Hsz. by rewrite size_filter -all_count => /all_filterP. 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