如何在coq中反过来使用定理a=b？

Question

假设我有一个定理 L 该说

forall x, x + 1 + 1 = x + 2.

如果我的目标是 a + 1 + 1 = b

我可以写一个命令 rewrite L 以求得 a + 2 = b

然而，如果我的目标是这样的形式 a + 2 = b

如何逆向应用定理来获得目标？ a + 1 + 1 = b?

Answer 1

说

rewrite <- L. (* Rewrite right to left *)

对于对称性，还有 rewrite -> L，这与 rewrite L 从左到右重写）。