diff --git a/Nevanlinna/stronglyMeromorphic.lean b/Nevanlinna/stronglyMeromorphic.lean
index 6f3f4a9..9b1beab 100644
--- a/Nevanlinna/stronglyMeromorphic.lean
+++ b/Nevanlinna/stronglyMeromorphic.lean
@@ -1,21 +1,69 @@
 import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
 
+
+/- Strongly MeromorphicAt -/
+
 def StronglyMeromorphicAt
   (f : ℂ → ℂ)
   (z₀ : ℂ) :=
-  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℕ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
+  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
 
-def MeromorphicAt.makeStronglyMeromorphic
+
+/- Strongly MeromorphicAt is Meromorphic -/
+theorem StronglyMeromorphicAt.meromorphicAt
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀) :
+  MeromorphicAt f z₀ := by
+  rcases hf with h|h
+  · use 0; simp
+    rw [analyticAt_congr h]
+    exact analyticAt_const
+  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
+    have : MeromorphicAt (fun z ↦ (z - z₀) ^ n • g z) z₀ := by
+      simp
+      apply MeromorphicAt.mul
+      apply MeromorphicAt.zpow
+      apply MeromorphicAt.sub
+
+      sorry
+    apply MeromorphicAt.congr this
+    rw [Filter.eventuallyEq_comm]
+    exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
+
+/- Strongly MeromorphicAt of positive order is analytic -/
+theorem StronglyMeromorphicAt.analytic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁f : StronglyMeromorphicAt f z₀)
+  (h₂f : 0 ≤ h₁f.meromorphicAt.order):
+  AnalyticAt ℂ f z₀ := by
+  sorry
+
+
+
+/- Make strongly MeromorphicAt -/
+
+def MeromorphicAt.makeStronglyMeromorphicAt
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
   ℂ → ℂ := by
   exact 0
 
-theorem makeStronglyMeromorphic
+
+theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
   {f : ℂ → ℂ}
   {z₀ : ℂ}
   (hf : MeromorphicAt f z₀) :
   StronglyMeromorphicAt hf.makeStronglyMeromorphic z₀ := by
   sorry
+
+
+theorem makeStronglyMeromorphic_eventuallyEq
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = hf.makeStronglyMeromorphicAt z := by
+  sorry