proposition: Lemma shift_plactcongr n u v : (u =Pl v) = (shiftn n u =Pl shiftn n v).
proof: Proof. apply/idP/idP. - apply: plact_map_in_incr => x y _ _. by rewrite !ltEnat /= ltn_add2l. - rewrite -{2}[u](shiftuK n) -{2}[v](shiftuK n) /shiftn. apply: plact_map_in_incr => x y /mapP[x0 Hx0 -> {x}] /mapP[y0 Hy0 -> {y}]. by rewrite !ltEnat /= ltn_add2l !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