proposition: Lemma is_col_dual T : sorted >%O (extract (in_tuple w) T) = sorted >%O (extract (in_tuple (revdual w)) (rev_set T)).
proof: Proof. Proof using. rewrite extract_rev_set. case: (extract _ _) => //= l0 l. rewrite -rev_sorted revK /sorted /=. apply eq_path => i j /=. by rewrite -ltEdual. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene