Theorem: bitvec_AddSub_1539_2 (Eval/bitvec_AddSub_1539_2.lean)

State before:
⊢ ∀ (x C : BitVec 64), x - C = x + -C
Tactic:
intros
State after:
x✝ C✝ : BitVec 64
⊢ x✝ - C✝ = x✝ + -C✝

State before:
x✝ C✝ : BitVec 64
⊢ x✝ - C✝ = x✝ + -C✝
Tactic:
bv_decide
State after:
no goals