我知道这一点，ring并且field可以用于某些等式，例如a + x = b + y. 我想知道是否有它的存在版本可以确定存在变量的值？
例如，我有以下内容：
r1, r2 : R
______________________________________(1/1)
r1*r1 + ?s = r2 * r2
我可以弄清楚这?s = r2 * r2 - r1 * r1可以解决这个问题。但是有没有这样的策略ering可以让 Coq 进行计算而不是我手动进行呢？
问问题
48 次