proposition: Lemma all_in_shufflel u v : predI (mem u) (mem v) =i pred0 -> all (fun s => filter (mem u) s == u) (shuffle u v).
proof: Proof. Proof using . elim: u v => [| a u IHu] /= v HI. by rewrite !andbT (eq_filter (a2 := pred0)) // filter_pred0. elim: v HI => [_ | b v IHv] /=. - rewrite !andbT inE eq_refl /=; apply/eqP; congr (a :: _). rewrite (eq_in_filter (a2 := predT)); first by rewrite filter_predT. by move => i /=; rewrite inE => ->; rewrite orbT. - move=> HI; rewrite all_cat. apply/andP; split; apply/allP=> x /mapP[s Hs ->{x}] /=. + rewrite !inE eq_refl /=; apply/eqP; congr (a :: _). have {}/IHu/allP Hu : [predI u & b :: v] =i pred0. move=> i; rewrite !inE; apply: negbTE. move/(_ i): HI; rewrite !inE => /negbT. by apply: contra => /andP[->]; rewrite orbT. case (boolP (a \in u)) => Ha. * rewrite (eq_filter (a2 := mem u)); first by apply/eqP; apply: (Hu _ Hs). move => i /=; rewrite inE. apply/idP/idP => [| ->]; last by rewrite orbT. by move/orP => [/eqP ->|]. * rewrite (eq_in_filter (a2 := mem u)); first by apply/eqP; apply: (Hu _ Hs). move => i /=; rewrite inE => Hi. apply/idP/idP; last by move ->; rewrite orbT. have /allP := perm_shuffle u (b :: v) => /(_ _ Hs)/perm_mem/(_ i). rewrite {}Hi /= mem_cat inE => /or3P[]; first by move ->. - move/eqP -> => /orP[] // /eqP Habs; exfalso. by move/(_ a): HI; rewrite !inE Habs !eq_refl. - move=> Hi /orP[] // /eqP Habs; move: Hi; rewrite Habs {i Habs} => Habs. by move/(_ a): HI; rewrite !inE Habs !eq_refl /= orbT. + have := HI b; rewrite !inE /= eq_refl /= andbT => ->. have /IHv/allP : [predI a :: u & v] =i pred0. move=> i /=; rewrite !inE; apply: negbTE. move/(_ i): HI; rewrite !inE => /negbT. by apply: contra => /andP[-> ->]; rewrite orbT. by apply. 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