# HG changeset patch
# User nipkow
# Date 1486024331 -3600
# Node ID 50f2f10ab57603949ca651be0e8b88d8735b9dd1
# Parent  1a4cb9403a100943adfb89039b564b8fb7bffcd7
tuned proof

diff -r 1a4cb9403a10 -r 50f2f10ab576 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Feb 01 21:09:47 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Feb 02 09:32:11 2017 +0100
@@ -222,12 +222,13 @@
 lemma ld_ld_1_less:
   assumes "x > 0" "y > 0" shows "1 + log 2 x + log 2 y < 2 * log 2 (x+y)"
 proof -
-  have 1: "2*x*y < (x+y)^2" using assms
+  have "2 powr (1 + log 2 x + log 2 y) = 2*x*y"
+    using assms by(simp add: powr_add)
+  also have "\<dots> < (x+y)^2" using assms
     by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
-  show ?thesis
-    apply(rule powr_less_cancel_iff[of 2, THEN iffD1])
-     apply simp
-    using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)
+  also have "\<dots> = 2 powr (2 * log 2 (x+y))"
+    using assms by(simp add: powr_add log_powr[symmetric] powr_numeral)
+  finally show ?thesis by simp
 qed
 
 corollary t_del_min_log: assumes "ltree t"