natAbs_natCast_sub_natCast_of_le

Mathlib.Data.Int.NatAbs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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