proposition: Lemma bijLR_inj : {in LRyam_set &, injective bijLR}.
proof: Proof. Proof using . move=> x y; rewrite !inE /bijLR => Hx Hy. case (boolP (is_skew_reshape_tableau P P1 x)) => /=; last by rewrite Hx. case (boolP (is_skew_reshape_tableau P P1 y)) => /=; last by rewrite Hy. move=> Hy1 Hx1 /(congr1 \val)/(congr1 to_word) /= {Hx1 Hy1 Hx Hy} => H. apply val_inj => /=. pose f := [fun s : seq nat => to_word (join_tab (hyper_stdtabn P1) (map (shiftn d1) (skew_reshape P1 P s)))]. have {H} Heq : f (std x) = f (std y) by rewrite /= H. have invf (s : yameval P2) : std s = sfilterleq d1 (f (std s)). have /= := join_stdtab_in_shuffle (stdtabnP (hyper_stdtabn P1)) (size_leq_skew_reshape (std s)). rewrite /size_tab. have /= -> := congr1 \val (shaped_hyper_stdtabnP P1). rewrite sumn_intpartn. have:= stdtabnP (hyper_stdtabn P1); rewrite /is_stdtab => /andP[_ /=]. move /shsh_sfilterleq => /[apply]. rewrite size_to_word (size_tab_stdtabn (hyper_stdtabn P1)) /sfilterleq /=. rewrite to_word_skew_reshape //. by rewrite size_std size_yameval sumn_diff_shape_intpartE. apply perm_stdE. - by rewrite perm_evalseq !eval_yameval. - by rewrite (invf x) (invf y) Heq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur