2
证明约序列的元素条件I有一个目标,看起来像这样:Coq的 - 在Ssreflect
x \in [seq (f v j) | j <- enum 'I_m & P v j] -> 0 < x
在上文中,f
是一个定义生成取决于v, j
和P v j
是一个不等式的溶液谓词将j限制在满足另一个不等式的指数上。
我已经证明,Goal : P v j -> (f v j > 0)
,但我怎么能用这个证明它适用于序列中的任何x
?我发现了几个相关的引理,如nthP
,它们引入了我很不熟悉的序列操作。
在此先感谢!