diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean
index 88666cf..691fc76 100644
--- a/Nevanlinna/meromorphicOn_decompose.lean
+++ b/Nevanlinna/meromorphicOn_decompose.lean
@@ -10,6 +10,17 @@ import Nevanlinna.mathlibAddOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
+theorem MeromorphicOn.order_ne_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsConnected U)
+  (h₂U : IsCompact U)
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
+  ∀ hz : z ∈ U, (h₁f z hz).order ≠ ⊤ := by
+
+  sorry
+
 
 theorem MeromorphicOn.decompose
   {f : ℂ → ℂ}
diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean
index bb40d85..de7cb10 100644
--- a/Nevanlinna/stronglyMeromorphicAt.lean
+++ b/Nevanlinna/stronglyMeromorphicAt.lean
@@ -348,7 +348,7 @@ theorem makeStronglyMeromorphic_id
   · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
 
 
-theorem StronglyMeromorphicAt.decompose
+theorem StronglyMeromorphicAt.eliminate
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (h₁f : StronglyMeromorphicAt f z₀)