natAbs_natCast_sub_natCast_of_ge

Mathlib.Data.Int.NatAbs

URI: https://scilib.ai/kg/mathlib#Int.natAbs_natCast_sub_natCast_of_ge

English

If b ≤ a (in ℕ), then natAbs(↑a − ↑b) = a − b.

Русский

Если b ≤ a (в ℕ), то natAbs(↑a − ↑b) = a − b.

LaTeX

$$$\\forall {a,b \\in \\mathbb{N}},\\; b \\le a \\Rightarrow \\operatorname{natAbs}(\\uparrow a - \\uparrow b) = a - b.$$$

Lean4

theorem natAbs_natCast_sub_natCast_of_ge {a b : ℕ} (h : b ≤ a) : Int.natAbs (↑a - ↑b) = a - b := by cutsat

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

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

Разделы

Аффилиация

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