Безболезненный способ показать простое неравенство над целым числом

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

Изучение соглашений об именовании Lean очень полезно для нахождения таких лемм.