exact Or.inl hsw
case inl
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfw : trunc n w = w
hxyulp : ulp n x ≤ 2 * y
ht : t = round (y - round (y - z))
hs₂ : t ≤ x → s = round (x - round (x - t))
hyw : y ≤ w
hwx : w ≤ x
hty : t ≤ y
hyx : y ≤ x
htx : t ≤ x
hs : s = round (x - round (x - t))
hfs : trunc n s = s
hft : trunc n t = t
hsy' : s ≤ round (x - round (x - y))
hsw : s ≤ w
⊢ s ≤ w ∨ w ≤ s ∧ y < s
no goals