Theorem: bitvec_AddSub_1176 (Eval/bitvec_AddSub_1176.lean)

State before:
⊢ ∀ (a b : BitVec 64), a + (0 - b) = a - b
Tactic:
intros
State after:
a✝ b✝ : BitVec 64
⊢ a✝ + (0 - b✝) = a✝ - b✝

State before:
a✝ b✝ : BitVec 64
⊢ a✝ + (0 - b✝) = a✝ - b✝
Tactic:
bv_decide
State after:
no goals