cases Nat.le_total (2 * b) a with
| inr hba' => have hf : round (a - b) = a - b := by
    apply hfaithful₀
    exact sterbenz hfa hfb hba hba'
  rewrite [hf, tsub_tsub_cancel_of_le hba]
  exact hfb
| inl hab' => apply sterbenz
  . exact hfa
  . exact trunc_round npos hfaithful₁ (a - b)
  . exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
  . have h : a ≤ 2 * (a - b) := by
      rewrite [Nat.mul_sub_left_distrib]
      rewrite [Nat.two_mul]
      rewrite [add_tsub_assoc_of_le hab']
      exact Nat.le_add_right _ _
    calc
      a = trunc n a             := by rw [hfa]
      _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
      _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
      _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
⊢ trunc n (a - round (a - b)) = a - round (a - b)
no goals