# HG changeset patch
# User nipkow
# Date 1601139552 -7200
# Node ID babd74b71ea89afe15406488bf4067ea0821051c
# Parent  0134a7d6ad56ca90c799ef09c78500d58df3747f
added lemma

diff -r 0134a7d6ad56 -r babd74b71ea8 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Sat Sep 26 17:04:51 2020 +0200
+++ b/src/HOL/Library/Tree.thy	Sat Sep 26 18:59:12 2020 +0200
@@ -153,6 +153,9 @@
 lemma neq_empty_subtrees[simp]: "{} \<noteq> subtrees t"
 by (cases t)(auto)
 
+lemma size_subtrees: "s \<in> subtrees t \<Longrightarrow> size s \<le> size t"
+by(induction t)(auto)
+
 lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
 by (induction t)(auto)