proposition: Lemma congr_bump r l : r != [::] -> is_row r -> bump r l -> r ++ [:: l] =Pl [:: bumped r l] ++ ins r l.
proof: Proof. Proof using. move=> Hnnil Hrow Hbump. have:= bump_inspos_lt_size Hrow Hbump; set pos := (inspos r l) => Hpos. move: (cat_take_drop pos r) (is_row_take pos Hrow) (is_row_drop pos Hrow). move HL : (take pos r) => L; move HR : (drop pos r) => R. case: R HR => [_ H| rpos R' HR Hr HrowL HrowR]. exfalso; move: H; rewrite -HL cats0 => /(congr1 size)/eqP. by rewrite size_take Hpos (ltn_eqF Hpos). have Hrpos : (rpos = bumped r l) by rewrite /bumped -{1}Hr nth_cat -HL size_take Hpos /pos ltnn subnn. apply: (@plact_trans _ _ (L ++ [:: rpos, l & R'])). - rewrite -Hr -catA; apply: plact_catr. rewrite cats1 rcons_cons; apply: (congr_row_2 HrowR). rewrite Hrpos; exact: lt_bumped. - have -> : ins r l = L ++ l :: R'. rewrite /ins -/pos -Hr; apply: set_nth_LxR. by rewrite -HL size_take Hpos. rewrite -[[:: rpos, l & R']]cat1s -![l :: R']cat1s !catA. apply: plact_catl. rewrite -Hrpos !cats1 cat1s rcons_cons. apply: congr_row_1; last by rewrite Hrpos; apply: lt_bumped. apply: (is_row_rcons HrowL). case/lastP: L HL {Hr HrowL} => [//= | L ll Hll]; rewrite last_rcons. have H : (size L) < pos. by have:= size_take pos r; rewrite Hpos Hll size_rcons => <-. have:= nth_lt_inspos H. by rewrite -(nth_take (n0 := pos) _ H) Hll nth_rcons ltnn eq_refl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr