proposition: Lemma std_shsh u v : is_std u -> is_std v -> all is_std (shsh u v).
proof: Proof. rewrite /is_std /shsh /shiftn => Hu Hv. apply/allP => s Hs. have /allP/(_ s Hs) := perm_shuffle u (shiftn (size u) v). rewrite perm_sym => /perm_trans; apply. have /allP/(_ s Hs)/eqP := all_size_shuffle u (shiftn (size u) v). rewrite size_map => -> {s Hs}. rewrite iotaD. apply: (@perm_trans _ (u ++ iota (size u) (size v))); last by rewrite perm_cat2r. rewrite perm_cat2l -{2}[size u]addn0 iotaDl. exact: perm_map. 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