proposition: Lemma plact2_ge L u v1 w v2 : v2 \in plact2 v1 -> [seq x <- u ++ v1 ++ w | (L >= x)%O] =Pl [seq x <- u ++ v2 ++ w | (L >= x)%O].
proof: Proof. Proof using. move/plact2P => [a] [b] [c] [Habc -> ->]. rewrite !filter_cat /=. apply: plact_catr; apply: plact_catl. case: (leP c L) => Hc; last exact: plact_refl. have /andP[Hab Hbc] := Habc. have HbL := le_trans Hbc Hc. rewrite HbL (le_trans (ltW Hab) HbL). apply: rule_gencongr => /=. by rewrite Habc !mem_cat inE eq_refl /= !orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr