proposition: Lemma leL_geLdualE u : filter leL u = from_revdual (filter geL (revdual u)).
proof: Proof. Proof using. rewrite /= filter_rev revK. by apply/eq_filter => i /=; rewrite -leEdual. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr