have ulp_eq : ulp n x = ulp n y := by
  rewrite [← ulp_trunc npos]
  apply le_antisymm
  . apply ulp_le_ulp
    exact h
  . rewrite [ulp_trunc npos]
    unfold ulp expt
    apply Nat.pow_le_pow_of_le_right two_pos
    apply tsub_le_tsub_right
    rewrite [Nat.size_le]
    apply Nat.lt_of_lt_of_le k
    exact next_trunc_le npos x
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
⊢ trunc n x = trunc n y
x y n : ℕ
npos : 0 < n
h : trunc n x ≤ y
k : y < next n (trunc n x)
ulp_eq : ulp n x = ulp n y
⊢ trunc n x = trunc n y