src/HOL/Library/Formal_Power_Series.thy

               add: fps_const_add [symmetric] fps_const_neg [symmetric]
                    fps_sin_deriv fps_cos_deriv algebra_simps)
   done
 
 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
-  by (auto simp add: fps_eq_iff fps_sin_def)
+  by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def)
 
 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c"
   by (auto simp add: fps_eq_iff fps_cos_def)
 
 definition "fps_tan c = fps_sin c / fps_cos c"