cases Nat.lt_or_ge x (2 ^ n) with
| inl uflow =>
  exact le_of_eq (trunc_add_half_ulp_eq_of_uflow uflow)
| inr no_uflow =>
  refine Nat.le_of_mul_le_mul_left ?_ two_pos
  rewrite [trunc_add_half_ulp_eq_of_no_uflow npos no_uflow]
  have h1 : x ≤ next n (trunc n x) := Nat.le_of_lt (lt_next_trunc npos x)
  have h2 : trunc n x ≤ x := trunc_le n x
  rewrite [Nat.two_mul, ← tsub_le_iff_left, add_tsub_assoc_of_le h1,
           Nat.add_comm, ← le_tsub_iff_right h2]
  exact hcorrect₁ x hhi
n x : ℕ
round : ℕ → ℕ
npos : 0 < n
hcorrect₁ : correct₁ n round
hhi : round x = next n (trunc n x)
⊢ trunc n x + ulp n x / 2 ≤ x
no goals