IMO 2002 #4

Stream: new members

[Nathan]

I proved the first part of this problem. I think I could delete a lot of the lemmas if I could prove

example {α : Type} (l : List α) (i : ℕ) (h : i < l.length) :
    have : i < l.reverse.length := by simp[h]
    l[l.length-1-i] = l.reverse[i] := sorry

and use it in conjunction with Nat.reverse_divisorsAntidiagonalList. I also had trouble with Fin/Finsets and a with casting naturals to rationals, so I think there's room for improvement there. The casting in theorem t1 is such a mess.

I'm happy with how lemma telescope turned out, which is a lemma for telescoping sums.

[Nathan]

This is the proof
IMO.lean

[Nathan]

this is the problem
Screenshot 2025-10-05 at 10.47.23 PM.png

[Henrik Böving]

Nathan said:

I proved the first part of this problem. I think I could delete a lot of the lemmas if I could prove

example {α : Type} (l : List α) (i : ℕ) (h : i < l.length) :
    have : i < l.reverse.length := by simp[h]
    l[l.length-1-i] = l.reverse[i] := sorry

That theorem is just by simp

[Nathan]

no way :joy: oh yeah and there's List.getElem_reverse how did i miss this

[Nathan]

thanks