have trunc_eq : trunc n x = x := by
  unfold trunc ulp expt
  rewrite [tsub_eq_zero_of_le uflow]
  rw [Nat.pow_zero, Nat.mul_one, Nat.div_one]
case inr
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
uflow : n ≥ Nat.size x
⊢ round x = trunc n x
case inr
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
uflow : n ≥ Nat.size x
trunc_eq : trunc n x = x
⊢ round x = trunc n x