. cases eq_or_ne b a with
  | inl eq => exact eq ▸ le_rfl
  | inr ne =>
    rewrite [bhi, alo]
    apply Nat.le_of_not_lt
    intro (lt_next_trunc : trunc n a < next n (trunc n b))
    have trunc_eq : trunc n a = trunc n b := by
      apply Nat.le_antisymm
      . rewrite [← trunc_idempotent npos a]
        exact trunc_le_trunc_of_lt_next_trunc npos lt_next_trunc
      . exact lolo
    have ulp_eq : ulp n a = ulp n b := by
      rw [← ulp_trunc npos b, ← ulp_trunc npos a, trunc_eq]
    apply Nat.lt_le_asymm (lt_of_le_of_ne hba ne)
    trans trunc n a + ulp n a / 2
    . exact le_midpoint_of_round_eq_trunc npos hcorrect₀ alo
    . rewrite [trunc_eq, ulp_eq]
      exact midpoint_le_of_round_eq_next_trunc npos hcorrect₁ bhi
case inr.inr
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
⊢ round b ≤ round a
no goals