proposition: Lemma rev_enum : enum 'I_(size (revdual w)) = rev [seq rev_ord_cast i | i : 'I_(size w)].
proof: Proof. Proof using. apply: (inj_map val_inj); rewrite /=. rewrite val_enum_ord map_rev -map_comp. rewrite [map (_ \o _) _](eq_map (g := (fun i => size w - i.+1) \o val)) //. rewrite map_comp val_enum_ord size_rev. apply: (eq_from_nth (x0 := 0)); first by rewrite size_rev size_map. move=> i; rewrite size_iota => Hi. rewrite nth_rev; last by rewrite size_map size_iota. rewrite (nth_iota _ _ Hi) add0n size_map (nth_map 0); last by rewrite size_iota; apply: irev_w. rewrite size_iota (nth_iota _ _ (irev_w Hi)). by rewrite add0n (subnSK Hi); rewrite subKn; last exact: ltnW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene