trig_scaffold: THEORY %------------------------------------------------------------------------ % % This is intended to only be used by the developers % %------------------------------------------------------------------------ BEGIN IMPORTING trig_ineq i : VAR posnat n : VAR nat a,b : VAR real % The following are in theory "trig" sin_eq_0 : LEMMA sin(a) = 0 IFF EXISTS (i: int): a = i * PI % The following is in theory "trig_approx" TAN : LEMMA 0 <= a AND a < PI/2 AND cos_lb(a) > 0 IMPLIES tan_ub(a) >= tan(a) AND tan_lb(a) <= tan(a) END trig_scaffold