∀ {f : ℂ → ℂ} {M R : ℝ} {z : ℂ},
  0 < M →
    DifferentiableOn ℂ f (Metric.ball 0 R) →
      Set.MapsTo f (Metric.ball 0 R) {z | z.re < M} →
        z ∈ Metric.ball 0 R → f 0 = 0 → ‖f z / (2 * ↑M - f z)‖ ≤ 1 / R * ‖z‖