constructor
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
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hst : s = t
hwt : w < t
⊢ trunc n (w - t) = w - t ∧ trunc n (t - w) = t - w
case inl.left
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
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hst : s = t
hwt : w < t
⊢ trunc n (w - t) = w - t

case inl.right
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
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hst : s = t
hwt : w < t
⊢ trunc n (t - w) = t - w