proposition: Lemma yam_std_inj : {in is_yam &, injective std}.
proof: Proof. move=> y w /=; rewrite !unfold_in -/is_yam => Hy Hw Hstd. apply perm_stdE; last exact Hstd. rewrite perm_evalseq. rewrite -(shape_RS_yam Hy) -(shape_RS_yam Hw). rewrite -(shape_RS_std y) -(shape_RS_std w). by rewrite Hstd. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple finfun finset path bigop order) tools partition Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact