cases Nat.lt_or_ge (a - b) (2 ^ n) with
| inl uflow =>
  apply b₁_of_round_eq
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact trunc_eq_self_of_uflow uflow
| inr no_uflow =>
  cases Nat.eq_zero_or_pos b with
  | inl bzero =>
    apply b₁_of_round_eq
    rewrite [bzero, tsub_zero]
    exact round_eq_of_trunc_eq npos hfaithful₀ hfa
  | inr bpos =>
    cases Nat.lt_or_ge (2 * b) a with
    | inr le_two_mul =>
      apply b₁_of_round_eq
      apply round_eq_of_trunc_eq npos hfaithful₀
      exact sterbenz hfa hfb hba le_two_mul
    | inl two_mul_lt =>
      rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
      . constructor
        . exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
        . exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
            hfa hfb two_mul_lt.le lt_round
      . exact b₁_of_round_eq eq_round.symm
      . constructor
        . cases Nat.lt_or_ge b (ulp n (a - b)) with
          | inl lt_ulp =>
            cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
            | inl ulp_eq_ulp =>
              exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
                npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
                round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
            | inr ulp_lt_ulp =>
              exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
                npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
                round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
          | inr ulp_le =>
            exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
              hfa hfb round_lt.le two_mul_lt.le ulp_le
        . exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
no goals