lean_workbook_plus_22881
ProvedProve: if
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22881 (a : ℝ) (h : a ≥ 1) : 9 * a ^ 10 ≥ 8 * a + 1 := by sorry
Source
Prove: if
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_22881 (a : ℝ) (h : a ≥ 1) : 9 * a ^ 10 ≥ 8 * a + 1 := by sorry