diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index 70ae011..4114ccb 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -363,6 +363,11 @@ theorem primitive_additivity
     apply DifferentiableOn.mono hf
     intro x hx
     simp
+    
+    let A₀ : dist x.re z₀.re ≤ dist x.re z₁.re + dist z₁.re z₀.re := by apply dist_triangle
+    
+
+
 
     sorry