diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index cca5e24..b2d28e6 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -303,10 +303,18 @@ theorem primitive_additivity
 
   let εx := rx - dist z₀.re z₁.re
   have hεx : εx > 0 := by
-    sorry
+    let A := hz₁.1
+    simp at A
+    dsimp [εx]
+    rw [dist_comm]
+    simpa
   let εy := ry - dist z₀.im z₁.im
   have hεy : εy > 0 := by
-    sorry
+    let A := hz₁.2
+    simp at A
+    dsimp [εy]
+    rw [dist_comm]
+    simpa
 
   use εx
   use hεx