proposition: Lemma pred0_std u v : is_std u -> [predI u & shiftn (size u) v] =i pred0.
proof: Proof. rewrite /is_std /shsh /shiftn => /perm_mem Hu i /=. rewrite !inE Hu mem_iota add0n /=. apply/negP => /andP[Hlt /mapP[j _ Hi]]. by move: Hlt; rewrite Hi -{2}[size u]addn0 ltn_add2l. 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