proposition: Lemma last_ins_lt r l b : (l < b -> last b r < b -> last b (ins r l) < b)%O.
proof: Proof. Proof using. rewrite -!nth_last => Hl Hlast. rewrite (set_nth_default l b); first last. have : (ins r l) != [::] by apply: set_nth_non_nil. by case : (ins r l). rewrite nth_set_nth size_set_nth /= maxnC /maxn ltnS. case: (leqP (size r) (inspos r l)) => H /=; first by rewrite eq_refl. case: (boolP ((size r).-1 == inspos r l)) => _; first exact: Hl. rewrite (set_nth_default b l) //. by move: Hlast; case r => /=; first by rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr