From 2e5d008857f585fc77936cf6248cea93aa7721b0 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 2 Aug 2024 07:16:38 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_primitive2.lean | 5 +++++
 1 file changed, 5 insertions(+)

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