rewrite [Nat.two_mul, ← tsub_le_iff_left, add_tsub_assoc_of_le h1,
         Nat.add_comm, ← le_tsub_iff_right h2]
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ trunc n x + next n (trunc n x) ≤ 2 * x
case inr
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
no_uflow : x ≥ 2 ^ n
h1 : x ≤ next n (trunc n x)
h2 : trunc n x ≤ x
⊢ next n (trunc n x) - x ≤ x - trunc n x