proposition: Lemma mem_shuffle_pred u v s Pu Pv: predI Pu Pv =i pred0 -> filter Pu s = u -> filter Pv s = v -> size s = size u + size v -> s \in shuffle u v.
proof: Proof. Proof using . move=> HI Hu Hv Hsz; have /all_filterP Hall := mem_shuffle_predU HI Hu Hv Hsz. elim: u v s Hu Hv {Hsz} Hall => [| a u' IHu] /= v s Hu Hv Hall. move: Hall => /all_filterP; rewrite (eq_in_filter (a2 := Pv)). by move <-; rewrite Hv mem_seq1. move=> i Hi /=. rewrite (_ : Pu i = false) //; apply/negP => HPu. have : i \in [seq x <- s | Pu x] by rewrite mem_filter HPu Hi. by rewrite Hu /= in_nil. elim: v s Hv Hu Hall => [// | b v IHv] /= s Hv Hu Hall. move: Hall => /all_filterP; rewrite (eq_in_filter (a2 := Pu)). by move <-; rewrite Hu mem_seq1. move=> i Hi /=. rewrite (_ : Pv i = false) ?orbF //; apply/negP => HPv. have : i \in [seq x <- s | Pv x] by rewrite mem_filter HPv Hi. by rewrite Hv /= in_nil. case: s Hu Hv Hall => [// | s0 s] /=. case: (boolP (Pu s0)) => Hs0 /=. - have -> : Pv s0 = false by move/(_ s0): HI; rewrite !inE Hs0. move=> [Ha]; subst s0 => Hu Hv Hall. rewrite mem_cat; apply/orP; left. by apply/mapP; exists s; first exact: IHu. - move=> Hu Hv {Hs0} /andP[Hs0 Hall]. move: Hv; rewrite Hs0 => [] [Htmp]; subst s0 => Hv. rewrite mem_cat; apply/orP; right. by apply/mapP; exists s; first exact: IHv. 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