English
In a tropical ordered additive monoid with top element, for any x and natural n, (n+1) times x equals x; i.e., x is idempotent under repeated tropical addition.
Русский
В тропическом упорядоченном моноиде с верхним элементом для любого x и натурального n выполняется (n+1) раз x = x; то есть x остаётся неизменным при повторном тропическом сложении.
LaTeX
$$$ (n+1) \cdot x = x $$$
Lean4
@[simp]
theorem succ_nsmul {R} [LinearOrder R] [OrderTop R] (x : Tropical R) (n : ℕ) : (n + 1) • x = x := by
induction n with
| zero => simp
| succ n IH =>
rw [add_nsmul, IH, one_nsmul, add_self]
-- TODO: find/create the right classes to make this hold (for enat, ennreal, etc)
-- Requires `zero_eq_bot` to be true
-- lemma add_eq_zero_iff {a b : tropical R} :
-- a + b = 1 ↔ a = 1 ∨ b = 1 := sorry
