Sum and difference coordinates

Over a commutative ring with invertible 2, the half-sum and half-difference of a pair have sum and difference equal to that pair.

theorem Prod.invOf_two_mul_add_sub {R : Type u_1} [CommRing R] [Invertible 2] (z : R × R) : (⅟2 * (z.1 + z.2) + ⅟2 * (z.1 - z.2), ⅟2 * (z.1 + z.2) - ⅟2 * (z.1 - z.2)) = z

The pair (⅟2 (x + y), ⅟2 (x - y)) is sent back to (x, y) by (a, b) ↦ (a + b, a - b).