lean_workbook_plus_54751
ProvedGiven and , prove that and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54751 (a b c d : ℝ) (h₁ : a + c ≥ b + d) (h₂ : a + b = c + d) : a ≥ d ∧ c ≥ b := by sorry
Source
Given and , prove that and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_54751 (a b c d : ℝ) (h₁ : a + c ≥ b + d) (h₂ : a + b = c + d) : a ≥ d ∧ c ≥ b := by sorry