Clarify some of the proofs and logic.

Clarify some of the proofs and logic.

Style: Avoid log1p for anything but the floating-point approximation
just to be extra-clear; write log(1 + ...) in the math otherwise.

Reverse order of branches to make the condition (<= lo x hi) clearer.