proposition: Lemma bump_bumprow_rconsE l r b : is_row (rcons r b) -> (l < b)%O -> bump r l -> let: (lres, rres) := bumprow r l in bumprow (rcons r b) l = (lres, rcons rres b).
proof: Proof. Proof using. move=> Hrowb Hl; have:= Hl => /inspos_rcons Hpos Hbump. have Hrow := is_row_rconsK Hrowb. have Hbumpb : bump (rcons r b) l by rewrite /bump last_rcons. rewrite (bump_bumprowE Hrow Hbump) (bump_bumprowE Hrowb Hbumpb). rewrite /bumped /ins -(inspos_rcons r Hl). have:= bump_inspos_lt_size Hrow Hbump => Hsize. by rewrite nth_rcons set_nth_rcons Hsize. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr