Theorem: Imo2000P2.lemma1 (Compfiles/Imo2000P2.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 0 < z
⊢ (-x + y + z) * (x - y + z) * (x + y - z) ≤ x * y * z
Tactic:
linarith [schur x y z (le_of_lt hx) (le_of_lt hy) (le_of_lt hz)]
State after:
no goals