nonneg_total — Mathlib

English

For d ∈ Nat and a,b ∈ Z√d, either a ≤ b or b ≤ a.

Русский

Для каждого d ∈ Nat и любых a,b ∈ Z√d верно: либо a ≤ b, либо b ≤ a.

LaTeX

$$a ≤ b ∨ b ≤ a$$

Lean4

protected theorem nonneg_total : ∀ a : ℤ√d, Nonneg a ∨ Nonneg (-a)
  | ⟨(x : ℕ), (y : ℕ)⟩ => Or.inl trivial
  | ⟨-[_+1], -[_+1]⟩ => Or.inr trivial
  | ⟨0, -[_+1]⟩ => Or.inr trivial
  | ⟨-[_+1], 0⟩ => Or.inr trivial
  | ⟨(_ + 1 : ℕ), -[_+1]⟩ => Nat.le_total _ _
  | ⟨-[_+1], (_ + 1 : ℕ)⟩ => Nat.le_total _ _

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