∀ (L : PeriodPair) (l₀ x : ℂ) (r : NNReal),
  0 < r →
    Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ →
      HasFPowerSeriesOnBall (L.derivWeierstrassPExcept l₀) (L.derivWeierstrassPExceptSeries l₀ x) x ↑r