src/HOL/Analysis/Extended_Real_Limits.thy

   unfolding Liminf_def eventually_at
 proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
   fix P d
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
-    by (auto simp: zero_less_dist_iff dist_commute)
+    by (auto simp: dist_commute)
   then show "\<exists>r>0. Inf (f ` (Collect P)) \<le> Inf (f ` (S \<inter> ball x r - {x}))"
     by (intro exI[of _ d] INF_mono conjI \<open>0 < d\<close>) auto
 next
   fix d :: real
   assume "0 < d"

   unfolding Limsup_def eventually_at
 proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
   fix P d
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
-    by (auto simp: zero_less_dist_iff dist_commute)
+    by (auto simp: dist_commute)
   then show "\<exists>r>0. Sup (f ` (S \<inter> ball x r - {x})) \<le> Sup (f ` (Collect P))"
     by (intro exI[of _ d] SUP_mono conjI \<open>0 < d\<close>) auto
 next
   fix d :: real
   assume "0 < d"