Issue Description:

I was trying to write tests for semantic conformance to the AdditiveArithmetic protocol along the lines of these when I realized we have almost no semantic constraints on conforming types. The docs for zero say:

— Zero is the identity element for addition. For any value, x + .zero == x and .zero + x == x.

But really—aside from the implied relationship between + and +=, - and -= based on their general descriptions—that's about it. One would expect a relationship between addition and subtraction, for example. @stephentyrone and I came up with a (probably incomplete) list of things that are missing from AdditiveArithmetic, e.g., subject to representational limitations (such as floating point precision or the inability to represent negative numbers):

• .zero - x is the additive inverse of x.

• + is commutative.

• + is associative.

• a + b == c implies c - b == a

• for a type that conforms to both AdditiveArithmetic and Comparable, a > b, c >= 0 implies a + c >= b + c, with equality only if rounding occurs.

Note: when these laws are documented they shouldn't be buried in the detailed descriptions of individual operations, like the quoted text about .zero above is.

Note: the longer we wait to document these laws, the more existing conformances are potentially “broken” by the introduction of the new semantic constraints.