proposition: Lemma shiftuK n : cancel (shiftn n) (map (subn^~ n)).
proof: Proof. move=> s; rewrite /shiftn -map_comp. rewrite (eq_map (g := id)); first by rewrite map_id. by move=> i /=; rewrite /= addKn. 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