∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r R : ℝ},
  0 < r →
    r ≤ R →
      ∀ {f : ℂ → E} {s : Set ℂ},
        s.Countable →
          ContinuousOn f (Metric.closedBall c R \ Metric.ball c r) →
            (∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) →
              ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z