Theorem: bitvec_AndOrXor_1705 (Eval/bitvec_AndOrXor_1705.lean)

State before:
⊢ ∀ (A B : BitVec 64), ((B == 0 || decide (A < B)) = true) = (A ≤ B + -1)
Tactic:
intros
State after:
A✝ B✝ : BitVec 64
⊢ ((B✝ == 0 || decide (A✝ < B✝)) = true) = (A✝ ≤ B✝ + -1)

State before:
A✝ B✝ : BitVec 64
⊢ ((B✝ == 0 || decide (A✝ < B✝)) = true) = (A✝ ≤ B✝ + -1)
Tactic:
bv_decide
State after:
no goals