ResidueTheoremOnRectangleWithSimplePole'

theorem ResidueTheoremOnRectangleWithSimplePole' {f : ℂ → ℂ} {z w p A : ℂ}    (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)    (pInRectInterior : Rectangle z w ∈ 𝓝 p) (fHolo : HolomorphicOn f (Rectangle z w \ {p}))    (near_p : (f - (fun s ↦ A / (s - p))) =O[𝓝[≠] p] (1 : ℂ → ℂ)) :    RectangleIntegral' f z w = A := by  set g := f - (fun s ↦ A / (s - p))  have gHolo : HolomorphicOn g (Rectangle z w \ {p}) := by    apply DifferentiableOn.sub fHolo    intro s hs    have : s - p ≠ 0 := sub_ne_zero.mpr hs.2    exact  DifferentiableWithinAt.div (by fun_prop) (by fun_prop) this  have := BddAbove_on_rectangle_of_bdd_near gHolo.continuousOn near_p  obtain ⟨h, ⟨hHolo, hEq⟩⟩ := existsDifferentiableOn_of_bddAbove pInRectInterior gHolo this  exact ResidueTheoremOnRectangleWithSimplePole zRe_le_wRe zIm_le_wIm pInRectInterior hHolo hEq