Compfiles/Usa1980P5.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1980, Problem 5

Let x,y,z be real numbers in the closed interval [0,1]. Show that

x/(y + z + 1) + y/(z + x + 1) + z/(x + y + 1) ≤ 1 + (1 - x)(1 - y)(1 - z).

Imports (2)
Imported by 1 file
  1. problem Usa1980P5.usa1980_p5 line 27 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, LE.le, HAdd.hAdd, HDiv.hDiv, HMul.hMul, HSub.hSub

    Proof uses: GE.ge, mul_nonneg, sub_nonneg_of_le, dite, Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 117 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

    Open to load the checked before-and-after goal states.