Theorem: bitvec_239 (Eval/bitvec_239.lean)

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

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