English
Let M be an AddCommMonoid with LinearOrder and IsOrderedCancelAddMonoid. Then the natural numbers act on M in an OrderedSMul fashion, i.e., n • a is monotone in a for all n.
Русский
Пусть M — добавочно-коммутативный моноид с линейным порядком и условия IsOrderedCancelAddMonoid; тогда по действию Nat на M задаётся упорядоченное умножение: n • a неубывает с a.
LaTeX
$$$ OrderedSMul\ N\ M. $$$
Lean4
instance orderedSMul [AddCommMonoid M] [LinearOrder M] [IsOrderedCancelAddMonoid M] : OrderedSMul ℕ M :=
OrderedSMul.mk'' fun n hn a b hab => by
cases n with
| zero => cases hn
| succ n =>
induction n with
| zero => dsimp; rwa [one_nsmul, one_nsmul]
| succ n ih => simp only [succ_nsmul _ n.succ, _root_.add_lt_add (ih n.succ_pos) hab]
