lean_workbook_plus_10448

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

For $n=3$ , prove that if $0 < a \leq b \leq c$ , then $c-a \geq 0$ , $c-b \geq 0$ , and $b-a \geq 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10448 (a b c : ℝ) (h₁ : 0 < a ∧ a ≤ b ∧ b ≤ c) :
  c - a ≥ 0 ∧ c - b ≥ 0 ∧ b - a ≥ 0   :=  by sorry

Source