1) Simplify comment -- one has to read the complete proof (available in ACL2)

in order to understand the algorithm anyway.

2) v->exp == -v->digits may be assumed.

3) Fix comment (v always shares data with a).