Compfiles/Imo1987P4.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1987, Problem 4

Prove that there is no function f : ℕ → ℕ such that f(f(n)) = n + 1987 for every n.

Imports (5)
Imported by 1 file
  1. problem Imo1987P4.imo1987_p4 line 32 source

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

    Statement uses: Not, Exists, Nat, Eq, HAdd.hAdd, OfNat.ofNat

    Proof uses: HMul.hMul, False, Function.Injective, Nat.add_right_cancel, Eq.symm, Eq.mp, congrArg, Set, SDiff.sdiff, Set.univ, Set.image, Union.union, Eq.mpr, id, congrFun', Set.image_sdiff, Set.sdiff_union_sdiff_cancel, Set.subset_univ, Set.image_mono, Set.ofPred and 38 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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