English
The real numbers form an ordered additive monoid: addition by a fixed element preserves order.
Русский
Действительные образуют упорядоченный аддитивный мономиод: при прибавлении фиксированного элемента порядок сохраняется.
LaTeX
$$$\text{IsOrderedAddMonoid}(\mathbb{R})\;:\; \text{(addition preserves order)}$$$
Lean4
instance instIsOrderedAddMonoid : IsOrderedAddMonoid ℝ where
add_le_add_left := by
simp only [le_iff_eq_or_lt]
rintro a b ⟨rfl, h⟩
· simp only [lt_self_iff_false, or_false, forall_const]
· refine fun c => Or.inr ?_
induction a using Real.ind_mk with
| _ a =>
induction b using Real.ind_mk with
| _ b =>
induction c using Real.ind_mk with
| _ c =>
simp only [mk_lt, ← mk_add] at *
change Pos _ at *
rwa [add_sub_add_left_eq_sub]
