proposition: Corollary yam_plactic_shape y z : is_yam y -> ( y =Pl z <-> (is_yam z /\ evalseq y = evalseq z)).
proof: Proof. move=> Hyam; split. - move=> HPl; split; first exact (is_yam_plactic Hyam HPl). rewrite -(shape_RS_yam Hyam) -(shape_RS_yam (is_yam_plactic Hyam HPl)). exact: plactic_shapeRS. - move=> [Hyamz Hsh]. apply Sch_plact. by rewrite (RS_yam Hyam) (RS_yam Hyamz) Hsh. 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