Theorem: BVDecide.Normalize.BitVec.le_ult (LeanSAT/Reflect/Tactics/Normalize/BitVec.lean)

State before:
w : Nat
x y : BitVec w
⊢ x.toNat.le y.toNat = ¬y.toNat.lt x.toNat
Tactic:
simp
State after:
no goals