proposition: Theorem RS_rev_uniq s : uniq s -> RS (rev s) = conj_tab (RS s).
proof: Proof. Proof using. move Hsz : (size s) => n. elim: n s Hsz => [| n IHn] s. by rewrite /RS /conj_tab; move=> /eqP/nilP -> _ /=. move=> Hsz Huniq. have:= size_rembig s; rewrite Hsz /= => {}/IHn/(_ (rembig_uniq Huniq)). rewrite (rembig_rev_uniq Huniq). have: shape (RS (rev s)) = conj_part (shape (RS s)). have Htr := is_tableau_RS (rev s); have Ht := is_tableau_RS s. apply: sumn_take_inj. exact: is_part_sht. exact: is_part_conj (is_part_sht _). move=> k. rewrite -Greene_col_RS -Greene_row_RS /Greene_col /Greene_row. rewrite Greene_rel_rev revK (Greene_rel_uniq _ Huniq). apply eq_Greene_rel => x y /=. by rewrite lt_def. case Hs: s Hsz => [// | s0 s'] Hsz. have [iu] := rembig_RS s0 s'; rewrite -Hs => Hrem; rewrite Hrem. case/lastP Hrs: s Hsz Hs => [// | t tn] _ Hs; rewrite -Hrs => Hsh Heq. have [iv] := rembig_RS tn (rev t); rewrite -rev_rcons -Hrs => HRSr. move: Hsh; rewrite {}HRSr. have Hpart := is_part_sht (is_tableau_RS (rembig s)). have: is_add_corner (shape (RS (rembig s))) iu. have := is_part_sht (is_tableau_RS s); rewrite Hrem shape_append_nth => Hparti. rewrite -(incr_nthK Hpart Hparti); apply (add_corner_decr_nth Hparti). rewrite del_rem_corner => //. by move: Hpart => /is_partP[]. move: Heq Hpart. move: (RS (rembig (rev s))) (RS (rembig s)) => tabr tab Hr. subst tabr => Hpart Hcorn Hsh. apply eq_from_shape_get_tab; first by rewrite shape_conj_tab. move => [r c]. rewrite (append_nth_conj_tab _ Hpart Hcorn). congr (get_tab (append_nth _ _ _) _). - apply: maxL_perm; rewrite -Hs -rev_rcons. by rewrite perm_sym -perm_rev. - move: Hsh. rewrite !shape_append_nth shape_conj_tab. rewrite conj_part_incr_nth //. exact: incr_nth_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene