oadd_lt_oadd_2 — Mathlib

English

If h1: NF(oadd e n1 o1) and (n1 : ℕ) < n2, then oadd e n1 o1 < oadd e n2 o2.

Русский

Если h1: NF(oadd(e,n1,o1)) и n1 < n2, то oadd(e,n1,o1) < oadd(e,n2,o2).

LaTeX

$$$NF(\mathrm{oadd}(e,n_1,o_1)) \land (n_1 : \mathbb{N}) < n_2 \Rightarrow \mathrm{oadd}(e,n_1,o_1) < \mathrm{oadd}(e,n_2,o_2)$$$

Lean4

theorem oadd_lt_oadd_2 {e o₁ o₂ : ONote} {n₁ n₂ : ℕ+} (h₁ : NF (oadd e n₁ o₁)) (h : (n₁ : ℕ) < n₂) :
    oadd e n₁ o₁ < oadd e n₂ o₂ := by
  simp only [lt_def, repr]
  refine lt_of_lt_of_le ((add_lt_add_iff_left _).2 h₁.snd'.repr_lt) (le_trans ?_ (le_add_right _ _))
  rwa [← mul_succ, mul_le_mul_iff_right₀ (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]

Похожие утверждения