# HG changeset patch
# User nipkow
# Date 1501576122 -7200
# Node ID fd89f97c80c22231442ffae02172379067a6c31c
# Parent  8a6a89d6cf2b65632ecdfd5d73d3b48eaeacf499
new lemma

diff -r 8a6a89d6cf2b -r fd89f97c80c2 src/HOL/Data_Structures/Tree23.thy
--- a/src/HOL/Data_Structures/Tree23.thy	Tue Aug 01 07:26:23 2017 +0200
+++ b/src/HOL/Data_Structures/Tree23.thy	Tue Aug 01 10:28:42 2017 +0200
@@ -40,4 +40,7 @@
 "bal (Node3 l _ m _ r) =
   (bal l & bal m & bal r & height l = height m & height m = height r)"
 
+lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
+by (induction t) auto
+
 end