sub_add_of_lt

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.sub_add_of_lt

English

If b < a for a,b ∈ ℕ⁺, then a - b + b = a.

Русский

Если b < a для a,b ∈ ℕ⁺, то a − b + b = a.

LaTeX

$$$$ \forall a,b \in \mathbb{N}_{>0},\; b < a \Rightarrow a - b + b = a $$$$

Lean4

theorem sub_add_of_lt {a b : ℕ+} (h : b < a) : a - b + b = a := by rw [add_comm, add_sub_of_lt h]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru