Theorem: bitvec_AddSub_1165 (Eval/bitvec_AddSub_1165.lean)

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

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