proposition: Lemma shuffleC u v : perm_eq (shuffle u v) (shuffle v u).
proof: Proof. Proof using . elim: u v => [| a u IHu] /= v; first by rewrite shuffle_nil perm_refl. elim: v => [| b v IHv] /=; first by rewrite perm_refl. set sa := (X in X ++ _); set sb := (X in _ ++ X). apply: (@perm_trans _ (sb ++ sa)); first by apply/permPl; apply: perm_catC. set sc := (X in perm_eq _ (X ++ _)). apply: (@perm_trans _ (sc ++ sa)). - rewrite perm_cat2r /sb /sc /= {sa sb sc}. by apply: perm_map; exact: IHv. - rewrite perm_cat2l /sa /= {sa sb sc}. by apply: perm_map; exact: IHu. 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