rw [← ulp_trunc npos b, ← ulp_trunc npos a, trunc_eq]
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
hba : b ≤ a
lolo : trunc n b ≤ trunc n a
lohi : trunc n b ≤ next n (trunc n a)
hihi : next n (trunc n b) ≤ next n (trunc n a)
bhi : round b = next n (trunc n b)
alo : round a = trunc n a
ne : b ≠ a
lt_next_trunc : trunc n a < next n (trunc n b)
trunc_eq : trunc n a = trunc n b
⊢ ulp n a = ulp n b
no goals