proposition: Theorem rembig_RS_last_big a v : RS (a :: v) = append_nth (RS (rembig (a :: v))) (maxL a v) (last_big (RS (a :: v)) (maxL a v)).
proof: Proof. Proof using. have: a :: v != [::] by []. move Hrem : (rembig (a :: v)) => rem; move: Hrem => /eqP; rewrite eq_sym. move/rembigP => /[apply]- [L] [b] [R] [-> Hav HL HR]. rewrite (maxL_LbR Hav HL (allLtnW HR)) Hav {a v Hav}. elim/last_ind: R HR => [/= _| R Rn IHR]. - rewrite cats0 cats1. rewrite [RS (rcons L b)]/RS rev_rcons /= -[RS_rev (rev L)]/(RS L). case HRS : (instab (RS L)) => [| tr0 tr /=]. + exfalso; move: HRS; case: (RS L) => [// | t0 t /=]. by case: (bumprow t0 b) => [[] u v]. + move: HRS; case HRSL : (RS L) => [// | t0 t /=]. * by move=> [<- <-] /=; rewrite eq_refl. * have Hrow: is_row (rcons t0 b). have := allLeq_is_row_rcons HL; rewrite HRSL. by apply; rewrite inE eq_refl orTb. rewrite (bumprow_rcons Hrow). by move=> [<- <-]; rewrite last_rcons eq_refl /=. - move=> Hmax; have HmaxR:= allLtn_rconsK Hmax; move: Hmax => /allLtn_last HRnb. rewrite -rcons_cons -!rcons_cat /RS !rev_rcons /=. rewrite -[RS_rev _]/(RS (L ++ b :: R)) -[RS_rev _]/(RS (L ++ R)). move/(_ HmaxR) : IHR. move Hlb : (last_big (RS (L ++ b :: R)) b) => lb IHR. move: Hlb => /eqP; rewrite eq_sym => /last_bigP Htmp. have Htmp2 : allLeq (to_word (RS (L ++ b :: R))) b. apply: (perm_allLeq (perm_RS (L ++ b :: R))). by rewrite allLeq_catE //= (allLtnW HmaxR) andbT HL /=. have {Htmp Htmp2} := Htmp (is_tableau_RS (L ++ b :: R)) Htmp2 => [] [] _. rewrite {}IHR => Hj. apply: (bisimul_instab (is_tableau_RS (L ++ R)) HRnb). + by apply: allLeq_is_row_rcons; rewrite allLeq_catE HL (allLtnW HmaxR). + by move=> j Hjlb; move/(_ j Hjlb): Hj; rewrite nth_set_nth /= (ltn_eqF Hjlb). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr