Theorem: bitvec_AndOrXor_1683_1 (Eval/bitvec_AndOrXor_1683_1.lean)

State before:
⊢ ∀ (a b : BitVec 64), ((decide (b < a) || a == b) = true) = (b ≤ a)
Tactic:
intros
State after:
a✝ b✝ : BitVec 64
⊢ ((decide (b✝ < a✝) || a✝ == b✝) = true) = (b✝ ≤ a✝)

State before:
a✝ b✝ : BitVec 64
⊢ ((decide (b✝ < a✝) || a✝ == b✝) = true) = (b✝ ≤ a✝)
Tactic:
bv_decide
State after:
no goals