Demostrar con Lean4 que en los anillos ordenados
\n\\[ 0 \u2264 b – a \u2192 a \u2264 b \\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Algebra.Order.Ring.Defs\r\nvariable {R : Type _} [StrictOrderedRing R]\r\nvariable (a b c : R)\r\n\r\nexample : 0 \u2264 b - a \u2192 a \u2264 b :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSe usar\u00e1n los siguientes lemas:
\n\\begin{align}
\n &0 + a = a \\tag{L1} \\\\
\n &b \u2264 c \u2192 (\u2200 a) [b + a \u2264 c + a] \\tag{L2} \\\\
\n &a – b + b = -a \\tag{L3}
\n\\end{align}
\nSupongamos que
\n\\[ 0 \u2264 b – a \\tag{1} \\]
\nLa demostraci\u00f3n se tiene por la siguiente cadena de desigualdades:
\n\\begin{align}
\n a &= 0 + a &&\\text{[por L1]} \\\\
\n &\u2264 (b – a) + a &&\\text{[por (1) y L2]} \\\\
\n &= b &&\\text{[por L3]}
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Algebra.Order.Ring.Defs\r\nvariable {R : Type _} [StrictOrderedRing R]\r\nvariable (a b c : R)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : 0 \u2264 b - a \u2192 a \u2264 b :=\r\nby\r\n intro h\r\n calc\r\n a = 0 + a := (zero_add a).symm\r\n _ \u2264 (b - a) + a := add_le_add_right h a\r\n _ = b := sub_add_cancel b a\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : 0 \u2264 b - a \u2192 a \u2264 b :=\r\n-- by apply?\r\nsub_nonneg.mp\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : 0 \u2264 b - a \u2192 a \u2264 b :=\r\nby simp\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (zero_add a : 0 + a = a)\r\n-- #check (add_le_add_right : b \u2264 c \u2192 \u2200 (a : R), b + a \u2264 c + a)\r\n-- #check (sub_add_cancel a b : a - b + b = a)\r\n-- #check (sub_nonneg : 0 \u2264 a - b \u2194 b \u2264 a)\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n