proposition: Lemma bumped_lt r b l : is_row r -> (l < b -> last b r < b -> bumped r l < b)%O.
proof: Proof. Proof using. rewrite -!nth_last /bumped => /is_rowP Hrow Hl Hlast. case: (ltnP (inspos r l) (size r)) => H. - rewrite (set_nth_default b l H). apply: (@le_lt_trans _ _ (nth b r (size r).-1)); last exact Hlast. apply: Hrow; move: H; case: (size r) => [// | s]. by rewrite ltnS /= => -> /=. - by rewrite (nth_default _ H). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr