Theorem: getBit_zero (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ getBit 0 q = finTwoEquiv q.modNat
Tactic:
simp_rw [getBit_apply, getBitRes_zero_apply]
State after:
no goals