--- 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"