Correctness [Step 2] follows from the derivation we gave.
We'll measure efficiency in terms of the number of recursive calls as a function of a. This is a good predictor of runtime as long as a b fits in a single integer variable. (Assumes the addition takes unit time.)
