proposition: Lemma nbump_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 = (Some b, rres).
proof: Proof. Proof using. move=> Hrowb Hl; have:= Hl => /inspos_rcons Hpos Hnbump. have Hrow := is_row_rconsK Hrowb. have Hbumpb : bump (rcons r b) l by rewrite /bump last_rcons. rewrite (nbump_bumprowE Hrow Hnbump) (bump_bumprowE Hrowb Hbumpb). rewrite /bumped /ins -(inspos_rcons r Hl). have:= nbump_inspos_eq_size Hrow Hnbump => Hsize. by rewrite nth_rcons set_nth_rcons Hsize eq_refl ltnn rcons_set_nth. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr