src/HOL/Library/BigO.thy

   apply (auto simp add: bigo_def)
   apply (rule_tac x = "abs c" in exI)
   apply (subst abs_of_nonneg) back back
   apply (rule setsum_nonneg)
   apply force
-  apply (subst setsum_mult)
+  apply (subst setsum_right_distrib)
   apply (rule allI)
   apply (rule order_trans)
   apply (rule setsum_abs)
   apply (rule setsum_mono)
   apply (rule order_trans)