have h : x - trunc n x < next n (trunc n x) - x := by
  rewrite [tsub_lt_iff_left (trunc_le n x)]
  rewrite [← add_tsub_assoc_of_le (le_of_lt (lt_next_trunc npos x))]
  unfold next
  rewrite [ulp_trunc npos]
  rewrite [lt_tsub_iff_left]
  rewrite [← Nat.add_assoc]
  rewrite [← Nat.div_mul_cancel ulp_even]
  rewrite [← mul_two, ← mul_two, ← add_mul]
  exact Nat.mul_lt_mul_of_pos_right h two_pos
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
⊢ round x = trunc n x
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₁ : correct₁ n round
h✝ : x < trunc n x + ulp n x / 2
no_uflow : n < Nat.size x
expt_pos : 0 < Nat.size x - n
ulp_even : 2 ∣ ulp n x
h : x - trunc n x < next n (trunc n x) - x
⊢ round x = trunc n x