Use the definitions from the standard library of Lean for the scalars

[sonmarcho]

Lean now defines types like UInt8, Int8, etc. We should use those, or at least define the scalars in terms of BitVec as it is a more natural representation of machine integers and also allows us to benefit from native support.

For instance, omega already supports reasoning about the bounds of bit vectors, meaning we don't have to do this work in scalar_tac:

example (x y : BitVec 8) : x.toNat + y.toNat ≤ 512 := by omega

We may want to wait a bit before updating the definitions, because there is good native support for BitVec, but not yet for the machine integers like UInt8 which are not properly handled by omega and bv_decide yet.