proposition: Theorem plact_from_yam sh w : is_part sh -> w =Pl std (hyper_yam sh) -> { y | is_yam_of_eval sh y & std y = w }.
proof: Proof. move=> Hsh. have := (plactic_RS w (std (hyper_yam sh))) => [] [H _]. move=> /H => /eqP HRS. pose Sh := IntPart Hsh. have Hyam : is_yam_of_eval Sh (RSmap w).2. rewrite /is_yam_of_eval is_yam_RSmap2 /=. rewrite -shape_RSmap_eq RSmapE HRS shape_RS_std. by rewrite (shape_RS_yam (hyper_yamP Hsh)) evalseq_hyper_yam. pose yimg := YamEval Hyam. have Hw : w = RSmapinv2 (RS (std (hyper_yam sh)), val yimg). rewrite -{1}[w]RSmapK. have -> : RSmap w = ((RSmap w).1, (RSmap w).2) by case RSmap. by rewrite RSmapE HRS. pose y := (@auxbij_inv Sh yimg). exists y. - by rewrite /is_yam_of_eval yamevalP eval_yameval /=. - rewrite -[LHS]RSmapK -[RHS]RSmapK. have RSE (x : seq nat) : RSmap x = (RS x, (RSmap x).2). by rewrite -RSmapE; case RSmap. rewrite RSE [RSmap w]RSE HRS. congr (RSmapinv2 (_, _)). + have := stdtab_of_yamP (hyper_yamP Hsh); rewrite /is_stdtab => /andP[Htab _]. apply/eqP; rewrite -plactic_RS. apply: std_plact. rewrite (yam_plactic_shape _ (yamevalP _)); split; first exact: hyper_yamP. by rewrite eval_yameval evalseq_hyper_yam. + by rewrite RSmap_std (_ : (RSmap y).2 = @auxbij Sh y) // f_invF. 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