I have a goal that looks like this:
x \in [seq (f v j) | j <- enum 'I_m & P v j] -> 0 < x
In the above, f
is a definition generating a solution of an inequality depending on v, j
and P v j
is a predicate restricting j to indices which satisfy another inequality.
I have already proven that Goal : P v j -> (f v j > 0)
, but how can I use this to prove that it holds for any x
in the sequence? I have found just a few relevant lemmas like nthP
which introduce sequence manipulation, which I'm very unfamiliar with.
Thanks in advance!
You need to use the
mapP
lemma (that characterizesmem
bership wrtmap
):