proposition: Lemma predLR_bij_LRsupport : pred_LRtriple T1 T2 bij_LRsupport.
proof: Proof. Proof using HTriple Hsh1 Hsh2. apply/LRtripleP => //=. have:= take_drop_langQ; rewrite -/w => /= [] [Htake Hdrop]. apply LRtriple_cat_langQ => //. - have Hpair := changeTtakeP shape_takeRS. rewrite (toDepRSPair Hpair) inE. by have/(congr1 (fun p => (val p).2)) := RStabinvK (RSTabPair Hpair) => /= ->. - have Hpair := changeTdropP shape_dropRS. rewrite (toDepRSPair Hpair) inE. by have/(congr1 (fun p => (val p).2)) := RStabinvK (RSTabPair Hpair) => /= ->. 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