Compfiles/UK2024R1P2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

British Mathematical Olympiad 2024, Round 1, Problem 2

The sequence of integers a₀, a₁, ⋯ has the property that for each i ≥ 2, aᵢ is either 2 * aᵢ₋₁ - aᵢ₋₂, or 2 * aᵢ₋₂ - aᵢ₋₁.

Given that a₂₀₂₃ and a₂₀₂₄ are consecutive integers, prove that a₀ and a₁ are consecutive.

Imports (2)
Imported by 1 file
  1. problem UK2024R1P2.uk2024_r1_p2 line 28 source

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

    Statement uses: Nat, Int, GE.ge, OfNat.ofNat, Or, Eq, HSub.hSub, HMul.hMul, abs

    Proof uses: LE.le, HAdd.hAdd, Nat.decreasingInduction, LT.lt, Eq.mp, congr, congrArg, add_tsub_cancel_right, Nat.Simproc.add_sub_le, of_decide_eq_true, Eq.refl, Bool, Bool.true, of_eq_true, Eq.trans, True, Function.swap, eq_true, True.intro, Neg.neg and 25 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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