lean_workbook_plus_78186
ProvedGiven three real positive real numbers , , such that , prove that at least one of , , does not exceed 1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78186 (a b c : ℝ) (habc : a * b * c = 1) : ∃ x y z : ℝ, x = a - 1 / b ∧ y = b - 1 / c ∧ z = c - 1 / a ∧ x ≤ 1 ∨ y ≤ 1 ∨ z ≤ 1 := by sorry
Source