假设我们有这样的事情:
假设x是实数.证明如果存在实数y,使得(y + 1)/(y-2)= x,则x <> 1".
如果以一种显而易见的方式制定它:forall x : R, (exists y, ((y + 1) * / (y - 2)) = x) -> x <> 1一个人很快遇到问题.
我们假设存在y这样的情况((y + 1) * / (y - 2)) = x).我错误地认为这也应该暗示这一点y <> 2吗？有没有办法在Coq中恢复这些信息？
当然,如果y存在,那么它不是2.如何在Coq中恢复这些信息 - 我是否需要明确地假设它(也就是说,无法以某种方式通过存在实例化来恢复它？).
当然,destruct H as [y]只是给我们((y + 1) * / (y - 2)) = x)了y : R,但现在我们不知道y <> 2.