Compfiles/Imo1976P6.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1976, Problem 6

The sequence u_0, u_1, u_2, ... is defined by: u_0 = 2, u_1 = 5/2, u_{n+1} = u_n(u_{n-1}^2 - 2) - u_1 for n = 1, 2, ... . Prove that ⌊u_n⌋ = 2^(2^n - (-1)^n)/3 for all positive n, where ⌊x⌋ denotes the greatest integer less than or equal to x.

Imports (2)
Imported by 1 file
  1. problem Imo1976P6.imo1976_p6 line 28 source

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

    Statement uses: Nat, Real, Eq, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd, HSub.hSub, HMul.hMul, HPow.hPow, GT.gt, Int.floor, Neg.neg

    Proof uses: Nat.twoStepInduction, Eq.mpr, Mathlib.Meta.NormNum.instAtLeastTwo, id, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Eq.rec, Mathlib.Meta.NormNum.IsNat, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.natPow_zero, Eq.symm, Mathlib.Meta.NormNum.IsNat.rpow_eq_pow, Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Inv.inv and 210 more

    238 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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