Theorem: getBitRes_zero_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q : BV (m + 1)
⊢ (getBitRes 0) q = (finTwoEquiv q.modNat, q.divNat)
Tactic:
simp_rw [getBitRes_zero, getBitResZero_apply]
State after:
no goals