Fast2Sum.v

Fast2Sum.v is a proof of the following procedure:

double Fast2Sum (double a, b) {
double s = a + b;
double r = b - (s - a);
return r + s; }

See A floating-point technique for extending the available precision by T. J. Dekker.

So obvious, right?