add_zero — Mathlib

English

For any nimber a, a + 0 = a.

Русский

Для любого нимбера a, a + 0 = a.

LaTeX

$$$\\\\forall a: \\\\mathrm{Nimber},\\\\ a + 0 = a.$$$

Lean4

protected theorem add_zero (a : Nimber) : a + 0 = a :=
  by
  apply le_antisymm
  · apply add_le_of_forall_ne
    · intro a' ha
      rw [Nimber.add_zero]
      exact ha.ne
    · intro _ h
      exact (Nimber.not_lt_zero _ h).elim
  · by_contra! h
    replace h := h
    have := Nimber.add_zero (a + 0)
    rw [add_left_inj] at this
    exact this.not_lt h
termination_by a

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