Theorem: flipBit_mergeBitRes_zero (Controlbits/BitResiduum.lean)

State before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ (flipBit 0) (mergeBitRes 0 b p) = finProdFinEquiv (p, bif b then 0 else 1)
Tactic:
simp_rw [flipBit_zero_apply, mergeBitRes_zero_divNat,
  mergeBitRes_zero_modNat, Bool.apply_cond (Fin.rev)]
State after:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ finProdFinEquiv (p, bif b then Fin.rev 1 else Fin.rev 0) = finProdFinEquiv (p, bif b then 0 else 1)

State before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ finProdFinEquiv (p, bif b then Fin.rev 1 else Fin.rev 0) = finProdFinEquiv (p, bif b then 0 else 1)
Tactic:
rfl
State after:
no goals