theorem congr_aux_1' (x : ℝ) : -1 / (↑x - 1 + Complex.I * ↑x + 1) = (Complex.I - 1) / (2 * ↑x)

theorem Complex.ne_iff (a b : ℂ) : a ≠ b ↔ a.re ≠ b.re ∨ a.im ≠ b.im

theorem congr_aux_1'' (x : ℝ) : -1 / (↑x - 1 + Complex.I * ↑x + 1) = (Complex.I - 1) / (2 * ↑x)