proposition: Lemma perm_shuffle u v : all (perm_eq (u ++ v)) (shuffle u v).
proof: Proof. Proof using . elim: u v => [| a u IHu] /= v; first by rewrite perm_refl. elim: v => [| b v /allP IHv] /=; first by rewrite cats0 perm_refl. rewrite all_cat; apply/andP; split; apply/allP => s /mapP[t Ht ->{s}] /=. - rewrite perm_cons. by move/(_ (b :: v)): IHu => /allP; apply. - apply: (@perm_trans _ (b :: v ++ a :: u)). + by apply/permPl; have /= := perm_catC (a :: u) (b :: v). + rewrite perm_cons perm_sym. move/(_ t Ht) : IHv; rewrite perm_sym => /perm_trans; apply. by apply/permPl; have /= := perm_catC (a :: u) v. 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