English
If x < y and z ≤ t, with t ≠ ⊥ and (t = ⊤ → z = ⊤ → x = ⊥), then x + z < y + t.
Русский
Если x < y и z ≤ t, причём t ≠ ⊥ и (t = ⊤ → z = ⊤ → x = ⊥), то x + z < y + t.
LaTeX
$$$\\\\forall {x y z t \\\\in \\\\mathrm{EReal}},\\\\ x < y \\\\land z \\le t \\\\land t \\neq \\bot \\\\land (t = \\top \\\\Rightarrow z = \\top \\\\Rightarrow x = \\bot) \\\\Rightarrow x + z < y + t$$$
Lean4
theorem add_lt_add_of_lt_of_le' {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hbot : t ≠ ⊥)
(htop : t = ⊤ → z = ⊤ → x = ⊥) : x + z < y + t :=
by
rcases h'.eq_or_lt with (rfl | hlt)
· rcases eq_or_ne z ⊤ with (rfl | hz)
· obtain rfl := htop rfl rfl
simpa
lift z to ℝ using ⟨hz, hbot⟩
exact add_lt_add_right_coe h z
· exact add_lt_add h hlt
