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