Details About PVS Trigonometry Library

%     trig_basic:
%     -----------
%         - definition of pi with crude upper and lower bounds
%         - definition of sin, cos, and tan
%         - pythagorean properties: sq(sin(a)) + sq(cos(a)) = 1 
%         - sum and difference of two angles
%         - double angle formulas
%         - negative properties, e.g. sin(-a)
%         - periodicity, e.g. sin(a) = sin(a + 2 * j * pi) 
%         - co-function identities, e.g. sin(pi/2 - a) = cos(a)
%         - location of zeros of trig functions
%
%      trig_values                            Lemma names
%      -----------                   ------------------------------------
%         - trig functions at 0      : sin_0     , cos_0     , tan_0 
%         - trig functions at pi/6   : sin_pi6   , cos_pi6   , tan_pi6 
%         - trig functions at pi/4   : sin_pi4   , cos_pi4   , tan_pi4 
%         - trig functions at pi/3   : sin_pi3   , cos_pi3   , tan_pi3 
%         - trig functions at pi/2   : sin_pi2   , cos_pi2   , tan_pi2 
%         - trig functions at pi     : sin_pi    , cos_pi    , tan_pi 
%         - trig functions at 2*pi/3 : sin_2pi3  , cos_2pi3  , tan_2pi3 
%         - trig functions at 3*pi/4 : sin_3pi4  , cos_3pi4  , tan_3pi4 
%         - trig functions at 5*pi/4 : sin_5pi4  , cos_5pi4  , tan_5pi4 
%
%      trig_ineq
%      ---------
%         - regions where functions are greater than 0
%         - regions where functions are less    than 0
%         - regions where functions are increasing
%         - regions where functions are decreasing
%
%      trig_extra
%      ----------
%         - reduction theorems
%         - sum and product identities
%         - half-angle identities and zeros
%         - triple angle formulas
%
%      trig_approx
%      -----------
%          - taylor series approximations to trig functions:
%               sin_approx(a,n): sum first n terms of taylor expansion of sin
%               cos_approx(a,n): sum first n terms of taylor expansion of cos
%       
%      tan_approx
%      ----------
%          - taylor series approximations for tangent
%
%      law_cosines
%      -----------
%         - the law of cosines in a coordinate geometry formulation
%
%      trig_degree
%      -----------
%         - trig functions that take arguments in degrees: sind, cosd
%         - defines conversions toRad, toDeg
%
%      trig_inverses
%      -------------
%         - defines inverse trig functions: arcsin, arccos, and arctan 
%
%      trig_rew
%      -------------
%         - Experimental auto-rewrite-theory background library