zohaze (Nov 28 2021 at 13:23): zohaze (Nov 28 2021 at 13:23):I have these four hypothesis and non empty list. May I write nth i2 (a::l) 0 >= nth i1 (a::l) 0?
H1 : max a (list_max l) <= a
H2: a <= max a (list_max l).
H3: nth i2 (a :: l) 0 < nth i1 (a :: l) 0
H4: nth (S i2) (a :: l) 0 < nth i1 (a :: l) 0
please use the triple backtick syntax for code fragments, i.e., write three backticks, then a newline and your code, then a newline and three backticks again. For example, like this (you can view the source of this answer)
H1 : max a (list_max l) <= a
also see: https://github.com/adam-p/markdown-here/wiki/Markdown-Cheatsheet#code-and-syntax-highlighting
Last updated: Oct 03 2023 at 21:01 UTC