如何轻松消解of_nat构造的自然数不等式证明目标？

当然有啦！在Lean中处理这类从自然数嵌入到整数的线性不等式，有几个非常直接的手段，完全不用复杂推导：

方法1：用整数的针对性引理 #

整数加法是保序的，两边同时加上相同的数不会改变不等式的方向，对应的引理是add_lt_add_iff_right（或者add_lt_add_iff_left，取决于你要消掉哪一边的项）。你可以直接用这个引理的逆方向来推导：

exact add_lt_add_iff_right.mp nltm

解释一下：add_lt_add_iff_right给出了等价关系 x + z < y + z ↔ x < y（其中x、y、z都是整数），这里我们的前提nltm是of_nat a₁ + 1 < of_nat a + 1，正好对应等价关系的右边，所以用.mp（modus ponens，从等价关系的前提推结论）就能直接得到我们要的of_nat a₁ < of_nat a。

方法2：用linarith战术一键解决 #

如果你不想记具体的引理名，Lean的linarith战术专门用来处理线性算术问题，它能自动识别这类简单的不等式变形，直接输入：

linarith

就能瞬间消解这个目标，非常适合快速处理这类基础证明步骤。

额外思路：转成自然数不等式处理 #

因为of_nat是从自然数到整数的保序嵌入，你也可以先把不等式转换回自然数的范畴再处理：

rw [← of_nat_lt] at nltm ⊢
-- 现在目标变成了 a₁ < a，前提变成了 a₁ + 1 < a + 1
exact add_lt_add_iff_right.mp nltm

不过这个方法多了一步转换，不如前两种直接，但如果后续涉及更多自然数的性质，这种思路也有用。

内容的提问来源于stack exchange，提问作者ScarletAmaranth