English
If a ∈ Z√d is nonnegative and its negation -a is also nonnegative, then a = 0.
Русский
Если a в Z√d неотрицательно и -a тоже неотрицательно, то a = 0.
LaTeX
$$$$\forall a \in \mathbb{Z}\sqrt{d},\; a \ge 0 \;\text{and}\; -a \ge 0 \Rightarrow a = 0.$$$$
Lean4
theorem nonneg_antisymm : ∀ {a : ℤ√d}, Nonneg a → Nonneg (-a) → a = 0
| ⟨0, 0⟩, _, _ => rfl
| ⟨-[_+1], -[_+1]⟩, xy, _ => False.elim xy
| ⟨(_ + 1 : Nat), (_ + 1 : Nat)⟩, _, yx => False.elim yx
| ⟨-[_+1], 0⟩, xy, _ => absurd xy (not_sqLe_succ _ _ _ (by decide))
| ⟨(_ + 1 : Nat), 0⟩, _, yx => absurd yx (not_sqLe_succ _ _ _ (by decide))
| ⟨0, -[_+1]⟩, xy, _ => absurd xy (not_sqLe_succ _ _ _ d_pos)
| ⟨0, (_ + 1 : Nat)⟩, _, yx => absurd yx (not_sqLe_succ _ _ _ d_pos)
| ⟨(x + 1 : Nat), -[y+1]⟩, (xy : SqLe _ _ _ _), (yx : SqLe _ _ _ _) =>
by
let t := le_antisymm yx xy
rw [one_mul] at t
exact absurd t (not_divides_sq _ _)
| ⟨-[x+1], (y + 1 : Nat)⟩, (xy : SqLe _ _ _ _), (yx : SqLe _ _ _ _) =>
by
let t := le_antisymm xy yx
rw [one_mul] at t
exact absurd t (not_divides_sq _ _)
