Compfiles/Egmo2023P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

European Girls' Mathematical Olympiad 2023, Problem 1

There are n ≥ 3 positive real numbers a_1, a_2, . . . , a_n. For each 1 ≤ i ≤ n we let b_i = (a_(i-1) + a_(i+1)) / a_i (here we define a_0 to be a_n and a_(n+1) to be a_1). Assume that for all i and j in the range 1 to n, we have a_i ≤ a_j if and only if b_i ≤ b_j. Prove that a_1 = a_2 = ... = a_n.

Imports (2)
Imported by 1 file
  1. problem Egmo2023P1.egmo2023_p1 line 28 source

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

    Statement uses: Nat, NeZero, GE.ge, OfNat.ofNat, Fin, Real, GT.gt, Eq, HDiv.hDiv, HAdd.hAdd, HSub.hSub, Iff, LE.le

    Proof uses: Exists, Finite.exists_min, Finite.exists_max, Trans.trans, rfl, Eq.mpr, id, congrArg, div_le_div_of_nonneg_right, add_le_add, le_of_lt, HMul.hMul, Eq.symm, two_mul, mul_div_cancel_right₀, ne_of_gt, le_refl, eq_of_le_of_ge, le_trans, Iff.mp and 1 more

    85 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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