m k : ℕ
⊢ bit0 (shiftl m k) = m * (2 ^ k * 2)
m k : ℕ
⊢ shiftl m (k + 1) = m * 2 ^ (k + 1)
show bit0 (shiftl m k) = m * (2 ^ k * 2)
no goals
m k : ℕ
⊢ bit0 (shiftl m k) = m * (2 ^ k * 2)
rw [bit0_val, shiftl_eq_mul_pow m k, mul_comm 2, mul_assoc]