English
With decidable equality, the equivalence (a ≠ b ↔ a < b) ↔ a ≤ b holds.
Русский
При разрешимой эквивалентности равенствa, выполняется эквивалентность (a ≠ b ↔ a < b) ↔ a ≤ b.
LaTeX
$$$(a \\neq b \\leftrightarrow a < b) \\leftrightarrow a \\le b$$$
Lean4
theorem min_def' (a b : α) : min a b = if b ≤ a then b else a :=
by
rw [min_def]
rcases lt_trichotomy a b with (lt | eq | gt)
· rw [if_pos lt.le, if_neg (not_le.mpr lt)]
· rw [if_pos eq.le, if_pos eq.ge, eq]
·
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]
-- Variant of `min_def` with the branches reversed.
-- This is sometimes useful as it used to be the default.
