lean_workbook_plus_77146
ProvedIf x<0 then and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77146 (x : ℝ) (hx : x < 0) : 1 - x > 0 ∧ 2 * x^7 < 0 := by sorry
Source
If x<0 then and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_77146 (x : ℝ) (hx : x < 0) : 1 - x > 0 ∧ 2 * x^7 < 0 := by sorry