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 is in theory "trig_basic" sin_eq_0 : LEMMA sin(a) = 0 IFF EXISTS (i: int): a = i * PI END trig_scaffold