Theorem: flipBit_zero_apply (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ (flipBit 0) q = finProdFinEquiv (q.divNat, q.modNat.rev)
Tactic:
simp_rw [flipBit_apply, getBit_zero, Nat.pow_eq, finTwoEquiv_apply,
  getRes_zero, mergeBitRes_zero, Bool.cond_not, Bool.cond_decide]
State after:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ finProdFinEquiv (q.divNat, if q.modNat = 1 then 0 else 1) = finProdFinEquiv (q.divNat, q.modNat.rev)

State before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ finProdFinEquiv (q.divNat, if q.modNat = 1 then 0 else 1) = finProdFinEquiv (q.divNat, q.modNat.rev)
Tactic:
rcases Fin.modNat_two_eq_zero_or_one q with (h | h) <;> simp_rw [h] <;> rfl
State after:
no goals