rewrite [round_eq_of_trunc_eq npos hfaithful₀ hfr₂]
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
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (round (a - b) - (a - b)) = a - b
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
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - (round (a - b) - (a - b)) = a - b