--- 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"