# HG changeset patch
# User nipkow
# Date 1242733932 -7200
# Node ID 3dde56615750825b2ab64aad024ec8c1417ba418
# Parent  5b7b9ba5868d46e3ab5841320d1410b6fd8ab933
new lemma

diff -r 5b7b9ba5868d -r 3dde56615750 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 18 23:43:36 2009 +0100
+++ b/src/HOL/List.thy	Tue May 19 13:52:12 2009 +0200
@@ -2913,6 +2913,10 @@
   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
 by (induct xs) (auto simp add:sorted_Cons)
 
+lemma sorted_nth_mono:
+  "sorted xs \<Longrightarrow> i <= j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i <= xs!j"
+by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
+
 lemma set_insort: "set(insort x xs) = insert x (set xs)"
 by (induct xs) auto