The type of angles #
In this file we define
Real.Angle to be the quotient group
ℝ/2πℤ and prove a few simple lemmas
about trigonometric functions and angles.
Suppose a function to angles is continuous on a connected set and never takes the values
π on that set. Then the values of the function on that set all have the same sign.