Compfiles/Usa1991P4.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1991, Problem 4

let $ a = \frac{m^{m+1} + n^{n+1}}{m^m + n^n} $ where $m$ and $n$ are positive integers. Prove that $a^m + a^n \geq m^m + n^n$.

Imports (2)
Imported by 1 file
  1. problem Usa1991P4.usa1991_p4 line 30 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, HDiv.hDiv, HAdd.hAdd, HPow.hPow, LE.le

    Proof uses: Eq.mpr, id, congrArg, le_of_lt, div_pos, add_pos', pow_pos, Iff.mpr, Nat.cast_pos', Finset.sum, Finset.range, HMul.hMul, HSub.hSub, Finset.mul_sum, Finset.sum_mul, Finset.sum_congr, rfl, Finset, Membership.mem, div_pow and 195 more

    227 instances, coercions and auxiliary constants left out.

    Tactic trace: 103 steps

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