Theorem: bitvec_152 (Eval/bitvec_152.lean)

State before:
⊢ ∀ (x : BitVec 64), x * -1 = 0 - x
Tactic:
intros
State after:
x✝ : BitVec 64
⊢ x✝ * -1 = 0 - x✝

State before:
x✝ : BitVec 64
⊢ x✝ * -1 = 0 - x✝
Tactic:
bv_decide
State after:
no goals