I have a list of natural numbers (b::l) and want to compare two values at two different indexes. Only available information is that both indexes are less than length l. How i should proceed? To find length of list might be helpful? Secondly, what more information i should have to perform comparision?

You can use the `nth`

function to get the two values.

I am also using nth function. I have two indexes k1 k2 both are less than length l. maximum of list is not equal zero. Want to prove nth 0 l d > nth (S k2) l d . How i can prove this? What more hypothesis i should add?

If you've already got that theorem stated in Coq, it might make the question clearer if you include it here as well.

Last updated: Sep 23 2023 at 15:01 UTC