Theorem: getRes_base (Controlbits/BitResiduum.lean)

State before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getRes i q = 0
Tactic:
rw [Fin.eq_zero i]
State after:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getRes 0 q = 0

State before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getRes 0 q = 0
Tactic:
rcases Fin.exists_fin_two.mp ⟨q, rfl⟩ with (rfl | rfl) <;> rfl
State after:
no goals