have hfc : round (a - round (a - b)) = a - round (a - b) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
d : ℕ
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
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d
d : ℕ
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
hfd : trunc n d = d
hba : b ≤ a
hbd : b ≤ d
hab : ulp n a ≤ 2 * b
hbc : b < round (a - round (a - b))
hdc : d ≤ round (a - round (a - b))
hfc : round (a - round (a - b)) = a - round (a - b)
⊢ trunc n (round (a - round (a - b)) - d) = round (a - round (a - b)) - d