Theorem: trunc_two_mul (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ trunc n (2 * x) = 2 * trunc n x
Tactic:
rw [← pow_one 2, trunc_pow_mul npos x 1]
State after:
no goals