lean_workbook_plus_60906
ProvedProve that is non-negative for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60906 : ∀ a : ℝ, 0 ≤ a ∧ a ≤ 2 → 0 ≤ (-2 * a + 4) / (a ^ 2 + 1) := by sorry
Source
Prove that is non-negative for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_60906 : ∀ a : ℝ, 0 ≤ a ∧ a ≤ 2 → 0 ≤ (-2 * a + 4) / (a ^ 2 + 1) := by sorry