CoRN.reals.fast.uneven_CRplus

The approximation function for CRplus results distributes a given error evenly among its two operands. This is a perfectly reasonable implementation choice, but it is conceptually arbitrary: any ratio works fine. Furthermore, when reasoning about particular uses of CRplus, different ratios can be more natural fits to the proof at hand. For instance, in the additivity proof for the Riemann integral implementation, having the error for the sum of two integrals distributed proportionally to the widths of the two contiguous ranges makes it nicely match the error for the full integral on both sides. For situations like these, we now do a very ad-hoc redefinition of addition with a user-specified error distribution ratio, and show that it is equivalent to the normal CRplus.