pianke (Jun 08 2022 at 11:18): pianke (Jun 08 2022 at 11:18):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?
Li-yao (Jun 08 2022 at 12:17):You can use the nth function to get the two values.
pianke (Jun 09 2022 at 14:09):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?
Julin S (Jun 10 2022 at 06:10):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: Apr 20 2024 at 14:01 UTC