case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t

case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t
x y z t : EReal
h1 : x < y
h2 : z < t
⊢ x + z < y + t
rcases eq_or_ne x ⊥ with (rfl | hx)
no goals
case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t
simp [h1, bot_le.trans_lt h2]
case inr.intro
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t
case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t
lift x to ℝ using ⟨h1.ne_top, hx⟩
no goals
case inr.intro
y z t : EReal
h2 : z < t
x : ℝ
h1 : ↑x < y
hx : ↑x ≠ ⊥
⊢ ↑x + z < y + t
calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
_ ≤ y + t := add_le_add_right h1.le _