lt_xor_cases — Mathlib

English

If a < b ⊕ c, then either a ⊕ c < b or a ⊕ b < c.

Русский

Если a < b ⊕ c, то либо a ⊕ c < b, либо a ⊕ b < c.

LaTeX

$$$ a < b \oplus c \Rightarrow a \oplus c < b \lor a \oplus b < c $$$

Lean4

theorem lt_xor_cases {a b c : ℕ} (h : a < b ^^^ c) : a ^^^ c < b ∨ a ^^^ b < c :=
  by
  obtain ha | hb | hc := xor_trichotomy <| Nat.xor_assoc _ _ _ ▸ xor_ne_zero.2 h.ne
  exacts [(h.asymm ha).elim, Or.inl <| Nat.xor_comm _ _ ▸ hb, Or.inr hc]

Похожие утверждения