proposition: Lemma extract_rev_set S : (extract (in_tuple (revdual w))) (rev_set S) = revdual (extract (in_tuple w) S).
proof: Proof. Proof using. rewrite !/extract /= !extractIE /rev_set rev_enum. rewrite filter_rev filter_map. rewrite (eq_filter (a2 := mem S)); first last. by move=> i /=; rewrite mem_imset; last exact rev_ord_cast_inj. rewrite map_rev -!map_comp; congr (rev _). apply: eq_map => i /=; rewrite !(tnth_nth inh) /=. rewrite nth_rev; last exact: irev_w. rewrite subnSK // subKn; last exact: ltnW. exact: set_nth_default. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene