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.