English
For any c, if Decidable, and a,b in Ordering, the equality (if c then a else b) = lt is equivalent to (if c then a = lt else b = lt).
Русский
Для любого c с разрешимостью, и a,b из Ordering, равенство (if c then a else b) = lt эквивалентно (if c then a = lt else b = lt).
LaTeX
$$$\\forall c\\ (\\text{Decidable } c)\\ (a,b:\\text{Ordering}),\\ ((\\text{if } c\\text{ then } a\\text{ else } b) = \\text{Ordering.lt}) = \\text{if } c\\ then a = \\text{Ordering.lt} \\\\ else b = \\text{Ordering.lt}$$$
Lean4
@[simp]
theorem ite_eq_lt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt := by by_cases c <;> simp [*]
