proposition: Lemma rev_is_ksupp_row P : (P \is a k.-supp[<=%O, in_tuple w]) = (rev_ksupp P \is a k.-supp[<=%O, in_tuple (revdual w)]).
proof: Proof. Proof using. rewrite !unfold_in size_rev_ksupp trivIset_setrev; congr [&& _, _ & _]. apply/forallP/forallP => Hall S; apply/implyP. - move=> /imsetP[T HT ->{S}]. rewrite -is_row_dual. by move/(_ T) : Hall; rewrite HT. - move=> HS; move/(_ (rev_set S)) : Hall. rewrite (_ : _ \in _); last by rewrite mem_imset; last exact rev_set_inj. by rewrite is_row_dual. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene