# HG changeset patch
# User nipkow
# Date 1523633102 -7200
# Node ID 9ecc78bcf1efa72c17408640efb6de213b8ad02f
# Parent  959b0aed2ce5a417cd85cddf949925bca827c216
added lemma

diff -r 959b0aed2ce5 -r 9ecc78bcf1ef src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 11 10:59:13 2018 +0200
+++ b/src/HOL/List.thy	Fri Apr 13 17:25:02 2018 +0200
@@ -4962,6 +4962,9 @@
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
 by(induction xs rule: induct_list012)(auto)
 
+lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
+by(auto simp: le_Suc_eq length_Suc_conv)
+
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
 lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [0..<n]"