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