cases lt_or_ge n (Nat.size x) with
| inr uflow =>
  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]
  rw [round_eq_of_trunc_eq npos hfaithful₀ trunc_eq, trunc_eq]
| inl no_uflow =>
  have expt_pos : 0 < (Nat.size x) - n := lt_tsub_of_add_lt_left no_uflow
  have ulp_even : 2 ∣ ulp n x := dvd_pow_self _ (ne_zero_of_lt expt_pos)
  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
  cases hfaithful₁ x with
  | inl lo => exact lo
  | inr hi => exfalso ; exact Nat.lt_le_asymm h $ hcorrect₁ x hi
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
⊢ round x = trunc n x
no goals