Compfiles/Imo1977P6.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1977, Problem 6

Suppose f : ℕ+ → ℕ+ satisfies f(f(n)) < f(n + 1) for all n. Prove that f(n) = n for all n.

Imports (2)
Imported by 1 file
  1. theorem Imo1977P6.imo1977_p6_nat line 36 source

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

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

    Proof uses: LE.le, Nat.recAux, Nat.zero_le, Nat.succ_le_of_lt, Trans.trans, HSub.hSub, le_tsub_of_add_le_right, Eq.rec, Nat.succ, tsub_add_cancel_of_le, le_trans, Nat.succ_le_succ, Eq.le, rfl, StrictMono, strictMono_nat_of_lt_succ, lt_of_le_of_lt, Nat.eq_of_le_of_lt_succ, Iff.mp, StrictMono.lt_iff_lt

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  2. problem Imo1977P6.imo1977_p6 line 54 source

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

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

    Proof uses: ite, Nat.toPNat', Imo1977P6.imo1977_p6_nat, Nat.casesAuxOn, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_right_of_eq_false, False, ite_eq_left_of_eq_true, zero_add, Eq.symm, Eq.mpr, id, ite_congr, Eq.refl, Not, ite_true and 3 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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