English
In a canonical ordered additive structure with bottom, the only element whose successor is the bottom (zero) is the bottom itself.
Русский
В канонически упорядоченной аддитивной структуре с нижним элементом единственный элемент, для которого следующий элемент равен нижнему, — это сам нижний элемент.
LaTeX
$$$\mathrm{WithBot.succ}(a) = 0 \iff a = \bot$$$
Lean4
@[simp]
theorem succ_eq_zero [AddZeroClass α] [OrderBot α] [CanonicallyOrderedAdd α] [One α] [NoMaxOrder α] [SuccAddOrder α]
{a : WithBot α} : WithBot.succ a = 0 ↔ a = ⊥ := by
cases a
· simp [bot_eq_zero]
· rename_i a
simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false]
by_contra h
simpa [h] using max_of_succ_le (a := a)
