proposition: Lemma plactic_filter_ge L u v : u =Pl v -> [seq x <- u | (L >= x)%O] =Pl [seq x <- v | (L >= x)%O].
proof: Proof. Proof using. move: v; apply: gencongr_ind; first exact: plact_refl. move=> a b1 c b2 Hu. rewrite (plact_ltrans Hu) {u Hu} => /plactruleP[]. - exact: plact1_ge. - rewrite -plact1I => /(plact1_ge L)-/(_ a c). by move/plact_ltrans <-; exact: plact_refl. - exact: plact2_ge. - rewrite -plact2I => /(plact2_ge L)-/(_ a c). by move/plact_ltrans <-; exact: plact_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr