Fcilitate proof of arithmetic on bitvectors by Alt-Ergo
A suggestion coming from the Spark team
Add three new lemmas on addition, subtraction and negation on bitvectors, that are used by Alt-Ergo. Remove them in the driver targetting SMTLIBv2.
Also remove upper bound in guard of lemma to_uint_sub_bounded which is not needed.