lt_add_cases — Mathlib

English

Let a, b, c be Nimbers. If a < b + c, then either a + c < b or a + b < c.

Русский

Пусть a, b, c — Nimber. Если a < b + c, то либо a + c < b, либо a + b < c.

LaTeX

$$$ \forall a,b,c \in \text{Nimber},\ a < b + c \Rightarrow (a + c) < b \lor (a + b) < c $$$

Lean4

theorem lt_add_cases {a b c : Nimber} (h : a < b + c) : a + c < b ∨ a + b < c :=
  by
  obtain ha | hb | hc := add_trichotomy <| add_assoc a b c ▸ add_ne_zero_iff.2 h.ne
  exacts [(h.asymm ha).elim, Or.inl <| add_comm c a ▸ hb, Or.inr hc]

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