proposition: Theorem congr_RS w : w =Pl (to_word (RS w)).
proof: Proof. Proof using. elim/last_ind: w => [/=| w l0]. rewrite /RS /to_word /=; exact: plact_refl. rewrite /RS rev_rcons /= -[RS_rev (rev w)]/(RS w) => H. apply: (@plact_trans _ _ (rcons (to_word (RS w)) l0)); first exact: plact_rcons. have:= is_tableau_RS w. elim: (RS w) l0 {H} => [/=| r0 t IHt] l0. rewrite /RS /to_word /= => _; exact: plact_refl. move=> /= /and4P[Ht0 Hrow0 _ Htab]. case (boolP (bump r0 l0)) => [Hbump | Hnbump]. - rewrite (bump_bumprowE Hrow0 Hbump); move/(_ (bumped r0 l0) Htab) : IHt. rewrite !to_word_cons -!cats1 /= -catA => IHt. rewrite (@plact_ltrans _ _ _ (flatten (rev t) ++ [:: bumped r0 l0] ++ (ins r0 l0))). + by rewrite catA; exact: plact_catl. + by apply: plact_catr; exact: congr_bump. - rewrite (nbump_bumprowE Hrow0 Hnbump) {IHt}. rewrite !to_word_cons -!cats1 -catA cats1. by apply: plact_catr; rewrite nbump_ins_rconsE; first exact: plact_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr