theorem upper_ne_int (x : UpperHalfPlane) (d : ℤ) : ↑x + ↑d ≠ 0

theorem aut_iter_deriv (d : ℤ) (k : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => 1 / (z + ↑d)) {z : ℂ | 0 < z.im}) (fun (t : ℂ) => (-1) ^ k * ↑k.factorial * (1 / (t + ↑d) ^ (k + 1))) {z : ℂ | 0 < z.im}

theorem aut_iter_deriv' (d : ℤ) (k : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => 1 / (z - ↑d)) {z : ℂ | 0 < z.im}) (fun (t : ℂ) => (-1) ^ k * ↑k.factorial * (1 / (t - ↑d) ^ (k + 1))) {z : ℂ | 0 < z.im}

theorem aut_contDiffOn (d : ℤ) (k : ℕ) : ContDiffOn ℂ (↑k) (fun (z : ℂ) => 1 / (z - ↑d)) {z : ℂ | 0 < z.im}

theorem iter_div_aut_add (d : ℤ) (k : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => 1 / (z - ↑d) + 1 / (z + ↑d)) {z : ℂ | 0 < z.im}) ((fun (t : ℂ) => (-1) ^ k * ↑k.factorial * (1 / (t - ↑d) ^ (k + 1))) + fun (t : ℂ) => (-1) ^ k * ↑k.factorial * (1 / (t + ↑d) ^ (k + 1))) {z : ℂ | 0 < z.im}

theorem exp_iter_deriv_within (n m : ℕ) : Set.EqOn (iteratedDerivWithin n (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑m * s)) {z : ℂ | 0 < z.im}) (fun (t : ℂ) => (2 * ↑Real.pi * Complex.I * ↑m) ^ n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑m * t)) {z : ℂ | 0 < z.im}