English
Let e ∈ ONote and n ∈ PNat. For all a1, a2 ∈ ONote, if a1 < a2 then oadd e n a1 < oadd e n a2. In words, the operation oadd with fixed e and n is strictly increasing in its right argument.
Русский
Пусть e ∈ ONote и n ∈ PNat. Для любых a1, a2 ∈ ONote, если a1 < a2, то oadd e n a1 < oadd e n a2. Иными словами, операция oadd с фиксированными e и n строго возрастает по правому аргументу.
LaTeX
$$$\forall e : ONote, \forall n : PNat, \forall a_1,a_2 : ONote,\; a_1 < a_2 \Rightarrow oadd\; e\; n\; a_1 < oadd\; e\; n\; a_2$$$
Lean4
theorem oadd_lt_oadd_3 {e n a₁ a₂} (h : a₁ < a₂) : oadd e n a₁ < oadd e n a₂ :=
by
rw [lt_def]; unfold repr
exact @add_lt_add_left _ _ _ _ (repr a₁) _ h _
