rw [trunc_pow_mul npos, hfa]
case hfa
n a b : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hba : b ≤ a
⊢ trunc n (2 ^ 1 * a) = 2 ^ 1 * a
no goals