Theorem: bitvec_AddSub_1614 (Eval/bitvec_AddSub_1614.lean)

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

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