equal
deleted
inserted
replaced
231 "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)" |
231 "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)" |
232 by auto |
232 by auto |
233 |
233 |
234 lemma REAL_SUB_INV: |
234 lemma REAL_SUB_INV: |
235 "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)" |
235 "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)" |
236 by (simp add: division_ring_inverse_diff real_divide_def) |
236 by (simp add: division_ring_inverse_diff divide_real_def) |
237 |
237 |
238 lemma REAL_DOWN: |
238 lemma REAL_DOWN: |
239 "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)" |
239 "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)" |
240 by (intro impI exI[of _ "d / 2"]) simp |
240 by (intro impI exI[of _ "d / 2"]) simp |
241 |
241 |