rewrite [← two_mul, ← pow_one 2]
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (a + a - (a - b)) ≤ 2 * a
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ round (2 ^ 1 * a - (a - b)) ≤ 2 ^ 1 * a