diff -r df1150ec6cd7 -r 2c86ea8961b5 src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -2052,6 +2052,17 @@
   shows   "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
   using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
 
+lemma asymp_equivD_strong:
+  assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<noteq> 0 \<or> g x \<noteq> 0) F"
+  shows   "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
+proof -
+  from assms(1) have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
+    by (rule asymp_equivD)
+  also have "?this \<longleftrightarrow> ?thesis"
+    by (intro filterlim_cong eventually_mono[OF assms(2)]) auto
+  finally show ?thesis .
+qed
+
 lemma asymp_equiv_compose [asymp_equiv_intros]:
   assumes "f \<sim>[G] g" "filterlim h G F"
   shows   "f \<circ> h \<sim>[F] g \<circ> h"