lean_workbook_plus_11894
ProvedProve that \n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11894 : ∀ n : ℝ, n ≠ 0 ∧ n + 5 ≠ 0 → 5 / (n * (n + 5)) = 1 / n - 1 / (n + 5) := by sorry
Source
Prove that \n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_11894 : ∀ n : ℝ, n ≠ 0 ∧ n + 5 ≠ 0 → 5 / (n * (n + 5)) = 1 / n - 1 / (n + 5) := by sorry