Theorem: mergeBitRes_zero_divNat_modNat (Controlbits/BitResiduum.lean)

State before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ ((mergeBitRes 0 b p).divNat, (mergeBitRes 0 b p).modNat) = (p, bif b then 1 else 0)
Tactic:
simp_rw [← finProdFinEquiv_symm_apply, Equiv.symm_apply_eq]
State after:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ mergeBitRes 0 b p = finProdFinEquiv (p, bif b then 1 else 0)

State before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ mergeBitRes 0 b p = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
exact mergeBitRes_zero
State after:
no goals