proposition: Lemma perm_shiftn_std n s : is_std s -> perm_eq (shiftn n s) (iota n (size s)).
proof: Proof. rewrite /is_std /shiftn -{2}(addn0 n) 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