Warmups · warm-up

mediumknown result, no worker yet

The minimum never exceeds the maximum

Theorem · min_le_max'

The minimum never exceeds the maximum: min⁡(a,b)≤max⁡(a,b)\min(a,b) \le \max(a,b).

Formal statement · Lean 4.lean
theorem min_le_max' (a b : Nat) : min a b ≤ max a b := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗