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 _ _
case inl.hab
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
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
case inl.hab
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
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a ≤ 2 * round (a - b)