Compfiles/Canada1998P5.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Canadian Mathematical Olympiad 1998, Problem 5

Let m be a positive integer. Define the sequence {aₙ} by a₀ = 0, a₁ = m, and aₙ₊₁ = m²aₙ - aₙ₋₁ for n ≥ 1. Prove that an ordered pair (a,b) of nonegative integers, with a ≤ b, is a solution of the equation

(a² + b²) / (ab + 1) = m²

if an only if (a,b) = (aₙ,aₙ₊₁) for some n ≥ 0.

Imports (2)
Imported by 1 file
  1. def Canada1998P5.A line 30 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Int

    6 instances, coercions and auxiliary constants left out.

  2. problem Canada1998P5.canada1998_p5 line 35 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Iff, Eq, HAdd.hAdd, HPow.hPow, HMul.hMul, Exists, And, Int, Canada1998P5.A

    Proof uses: Nat.recAux, id, Eq.mpr, congrArg, rfl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.zero_pow, Mathlib.Tactic.Ring.Common.const_pos, Bool, Nat.ble, Mathlib.Tactic.Ring.Common.pow_zero, Mathlib.Tactic.Ring.Common.zero_mul and 109 more

    160 instances, coercions and auxiliary constants left out.

    Tactic trace: 83 steps

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