lean - 显示整数上的简单不等式的无痛方法

Question

我有以下状态：

a : ℕ,
a_1 : ℕ,
nltm : of_nat a_1 + 1 < of_nat a + 1
⊢ of_nat a_1 < of_nat a

请注意of_nat构造Z.

有没有一种无痛的方式来实现目标？

Answer 1

这是lt_of_lt_add_right：

open int
example (a a_1 : ℕ) (nltm : of_nat a_1 + 1 < of_nat a + 1) : of_nat a_1 < of_nat a :=
lt_of_add_lt_add_right nltm

学习精益命名约定对于找到这样的引理非常有帮助。