¹The function we name arctan is just the inverse tangent function which takes the different quandrants into account. We will assume it returns the value of the angle from the positive x-axis in the range [0, 2π). The details of the function are out of scope of the proof, but we note that such functions exist as this C function: http://www.cplusplus.com/reference/clibrary/cmath/atan2/