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