Demostrar con Lean4 que, en los anillos ordenados, \[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by sorry
Demostrar con Lean4 que en los anillos ordenados \[ 0 ≤ b - a → a ≤ b \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : 0 ≤ b - a → a ≤ b := by sorry
Demostrar con Lean4 que en los anillos ordenados se verifica que \[ a ≤ b → 0 ≤ b - a \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : a ≤ b → 0 ≤ b - a := by sorry