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