lean_workbook_plus_13792
Provedso
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13792 : ∀ x y : ℝ, x^6 + y^5 ≤ x + 1 ↔ y^5 ≤ x + 1 - x^6 := by sorry
Source
so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_13792 : ∀ x y : ℝ, x^6 + y^5 ≤ x + 1 ↔ y^5 ≤ x + 1 - x^6 := by sorry