trig_props: THEORY
BEGIN

%   analysis: LIBRARY "../analysis"

   IMPORTING power_series_deriv[real], 
             trig_fun, analysis@derivative_props, analysis@deriv_domain


   n: VAR nat
   x: VAR real

   sin_derivable: LEMMA derivable?(sin);

   deriv_sin    : THEOREM deriv(sin)(x) = cos(x)

   cos_derivable: LEMMA derivable?(cos);

   deriv_cos    : THEOREM deriv(cos)(x) = -sin(x)

   sin2_cos2_derivable: LEMMA derivable?(sin*sin+cos*cos)

   sin2_cos2    : THEOREM sin*sin + cos*cos = const_fun(1)

   sin_cos_one  : THEOREM sin(x)*sin(x) + cos(x)*cos(x) = 1

   sin_lt_1     : LEMMA abs(sin(x)) <= 1

END trig_props