Compfiles/Usa1993P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1993, Problem 1

For each integer n ≥ 2, determine whether a or b is larger, where a and b are positive real numbers satisfying

aⁿ = a + 1, b²ⁿ = b + 3a.

Imports (2)
Imported by 1 file
  1. determine Usa1993P1.a_is_larger line 28 source

    no axioms what this means

    Statement uses: Nat, Bool

    Proof uses: Bool.true

  2. problem Usa1993P1.usa1993_p1 line 30 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Real, LT.lt, Eq, HPow.hPow, HAdd.hAdd, HMul.hMul, ite, Bool, Usa1993P1.a_is_larger, Bool.true

    Proof uses: Eq.mpr, id, Eq.trans, True, ite_congr, eq_self, Eq.refl, Not, ite_true, HSub.hSub, Iff.mp, abs, abs_eq_iff_mul_self_eq, congrArg, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne and 113 more

    154 instances, coercions and auxiliary constants left out.

    Tactic trace: 46 steps

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