# HG changeset patch
# User nipkow
# Date 1477565695 -7200
# Node ID f8be2208e99cfbdd9d5be93b272b4f623f8d1bef
# Parent  c0d5e78eb6471847921a4466cbbb538c6e6d3e11
added lemma

diff -r c0d5e78eb647 -r f8be2208e99c src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Oct 26 22:40:28 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Thu Oct 27 12:54:55 2016 +0200
@@ -141,6 +141,9 @@
 lemma height_map_tree[simp]: "height (map_tree f t) = height t"
 by (induction t) auto
 
+lemma height_le_size_tree: "height t \<le> size (t::'a tree)"
+by (induction t) auto
+
 lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)"
 proof(induction t)
   case (Node l a r)