Compfiles/Imo1993P5.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1993, Problem 5

Does there exist a function f : ℕ → ℕ such that i) f(1) = 2 ii) f(f(n)) = f(n) + n for all n ∈ ℕ iii) f(n + 1) > f(n) for all n ∈ ℕ?

Imports (2)
Imported by 1 file
  1. determine Imo1993P5.DoesExist line 31 source

    no axioms what this means

    Statement uses: Bool

    Proof uses: Decidable.decide, True

    1 instances, coercions and auxiliary constants left out.

  2. abbrev Imo1993P5.Good line 33 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: And, Eq, OfNat.ofNat, HAdd.hAdd, LT.lt

    4 instances, coercions and auxiliary constants left out.

  3. lemma Imo1993P5.imo_1993_p5_N line 37 source

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

    Statement uses: Exists, Nat, And, Eq, OfNat.ofNat, HAdd.hAdd, LT.lt

    Proof uses: Real, Real.goldenRatio, Eq.refl, HMul.hMul, HPow.hPow, Eq.mpr, id, congrArg, Eq.symm, one_mul, Nat.cast_mul, add_mul, congrFun', Nat.cast_one, dite, Iff.mpr, mul_left_inj', ne_of_gt, Nat.cast_pos', Real.goldenRatio_sq and 200 more

    211 instances, coercions and auxiliary constants left out.

    Tactic trace: 136 steps

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

  4. problem Imo1993P5.imo1993_p5 line 158 source

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

    Statement uses: Iff, Eq, Bool, Imo1993P5.DoesExist, Bool.true, Exists, Nat, Imo1993P5.Good

    Proof uses: Eq.mpr, id, Eq.trans, True, congrFun', congrArg, decide_true, eq_self, true_iff, And, OfNat.ofNat, HAdd.hAdd, LT.lt, Imo1993P5.imo_1993_p5_N, Exists.intro, And.intro

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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