lean_workbook_plus_14932
ProvedShow by induction.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14932 : ∀ m : ℕ, (1 : ℝ) / (m + 1) < 1 / (3 * m + 2) + 1 / (3 * m + 3) + 1 / (3 * m + 4) := by sorry
Source
Show by induction.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14932 : ∀ m : ℕ, (1 : ℝ) / (m + 1) < 1 / (3 * m + 2) + 1 / (3 * m + 3) + 1 / (3 * m + 4) := by sorry