Declare index for ordered array

Stream: Is there code for X?

[Teddy Baker]

I am trying to define an ordered array or list, namely the list of ordered divisors of a given number n. I'd like to know if, given a list or array called div, there is a convenient notation to declare an index for that array. Also, I would like to know how to define the property that the given array is ordered, i.e. given indices i > j we have div[i]>div[j].

Update: I found the answer in the arrays section of the lean manual, which says that you can declare an index with i : Fin div.size. However, when I try to use this as an index, I have encountered an error saying that I must prove that this index is in bounds, which should be obvious from its definition. So I am still confused.