私はそれを知ってringおり、fieldのようないくつかの等式で使用できますa + x = b + y。存在変数の値を決定できる存在バージョンがあるかどうか疑問に思っていますか?
たとえば、次のものがあります。
r1, r2 : R
______________________________________(1/1)
r1*r1 + ?s = r2 * r2
?s = r2 * r2 - r1 * r1これで解決することがわかります。eringしかし、私が手動で計算する代わりに、Coq に計算をさせることができるような戦術はありますか?