--- a/src/HOL/Groups.thy Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Groups.thy Mon Jul 20 23:12:50 2015 +0100
@@ -1372,6 +1372,15 @@
end
+lemma dense_eq0_I:
+ fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
+ shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
+ apply (cases "abs x=0", simp)
+ apply (simp only: zero_less_abs_iff [symmetric])
+ apply (drule dense)
+ apply (auto simp add: not_less [symmetric])
+ done
+
hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>