add_lt_add_right — Mathlib

English

If x < y and z ≠ ⊤, then x + z < y + z.

Русский

Если x < y и z ≠ ⊤, то x+z < y+z.

LaTeX

$$$ \forall x,y,z: \mathrm{PartENat}, x < y \land z \neq \top \Rightarrow x+z < y+z $$$

Lean4

protected theorem add_lt_add_right {x y z : PartENat} (h : x < y) (hz : z ≠ ⊤) : x + z < y + z :=
  by
  rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩
  rcases ne_top_iff.mp hz with ⟨k, rfl⟩
  induction y using PartENat.casesOn
  · rw [top_add]
    exact_mod_cast natCast_lt_top _
  intro h
  norm_cast at h
  exact_mod_cast add_lt_add_right h _

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