proposition: Lemma plactic_filter_lt u v : u =Pl v -> filter ltL u =Pl filter ltL v.
proof: Proof. Proof using. move=> H; rewrite [filter _ u]ltL_gtLdualE [filter _ v]ltL_gtLdualE. rewrite -plact_from_dualE; apply: plactic_filter_gt. by rewrite -plact_dualE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr