proposition: Lemma card_LRtab_set_leq (P : seq nat) : #|[set Q in (LRsupport U1 U2) | (shape Q == P)]| <= #|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
proof: Proof. Proof using Hsh1 Hsh2. rewrite /LRsupport. have Hsimpl A B C : [set Q in (LRsupport A B) | (shape Q == C)] = [set Q : stdtabn (d1 + d2) | pred_LRtriple A B Q & (shape Q == C)]. apply/setP => Q; rewrite /LRsupport 2!inE [RHS]inE. by congr (_ && _); rewrite LRtriple_fastE. rewrite !{}Hsimpl. rewrite -(card_in_imset (f := bij_LRsupport)). - apply subset_leqif_cards; apply/subsetP => Qres /imsetP[Q]. rewrite inE => /andP[Hpred /eqP <-] -> {Qres}. rewrite inE; apply/andP; split. + exact: predLR_bij_LRsupport. + by rewrite shape_bij_LRsupport. - move=> Q1 Q2; rewrite inE => /andP[HQ1 /eqP HshQ1]. rewrite inE => /andP[HQ2 /eqP]; rewrite -HshQ1 {HshQ1} => Heqsh. move=>/(congr1 \val); rewrite /=. set w1 := (X in changeUT _ _ X). set w2 := (X in _ = (RStab (changeUT _ _ X)).2) => Heq1. have : RS w1 = RS w2. rewrite -!RSmapE /w1 /w2 !RSmapinv2K; first last. + rewrite /is_RSpair yamtabP /=; last by apply: is_part_sht; exact: stdtabP. by rewrite yam_of_stdtabP //= shape_yamtab shape_yam_of_stdtab. + rewrite /is_RSpair yamtabP /=; last by apply: is_part_sht; exact: stdtabP. by rewrite yam_of_stdtabP //= shape_yamtab shape_yam_of_stdtab. + by rewrite /= Heqsh. have:= take_drop_langQ HQ1. have:= plact_changeUT (shape_takeRS HQ1) (shape_dropRS HQ1); rewrite -/w1. rewrite plactic_RS => /eqP <- [HQ1take HQ1drop]. have:= take_drop_langQ HQ2. have:= plact_changeUT (shape_takeRS HQ2) (shape_dropRS HQ2); rewrite -/w2. rewrite plactic_RS => /eqP <- [HQ2take HQ2drop]. rewrite -!RStabE => Heq2. have {Heq1 Heq2 HQ1take HQ1drop HQ2take HQ2drop} Heq : w1 = w2. rewrite -(changeUTK HQ1take HQ1drop) -(changeUTK HQ2take HQ2drop). congr changeUT. rewrite -(RStabK (changeUT T1 T2 w1)) -(RStabK (changeUT T1 T2 w2)). congr RStabinv. apply val_inj; move: Heq1 Heq2 => /=. case: (RStabmap (changeUT T1 T2 w1)) => A1 B1. by case: (RStabmap (changeUT T1 T2 w2)) => A2 B2 /= -> ->. apply val_inj. rewrite /= -(yam_of_stdtabK (stdtabnP Q1)) -(yam_of_stdtabK (stdtabnP Q2)). congr stdtab_of_yam. have:= RSmapinv2K (RSpairyamQ Q1); rewrite -/w1 Heq /w2. by rewrite (RSmapinv2K (RSpairyamQ Q2)) => [] [_ ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly