equal
deleted
inserted
replaced
56 by simp |
56 by simp |
57 |
57 |
58 lemma realpow_two_diff: |
58 lemma realpow_two_diff: |
59 "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
59 "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
60 apply (unfold real_diff_def) |
60 apply (unfold real_diff_def) |
61 apply (simp add: ring_simps) |
61 apply (simp add: algebra_simps) |
62 done |
62 done |
63 |
63 |
64 lemma realpow_two_disj: |
64 lemma realpow_two_disj: |
65 "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" |
65 "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" |
66 apply (cut_tac x = x and y = y in realpow_two_diff) |
66 apply (cut_tac x = x and y = y in realpow_two_diff) |