src/HOL/ex/Sum_of_Powers.thy

 lemma sum_of_squares_nat: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) div 6"
 proof -
   from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
     by (auto simp add: field_simps)
   then have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
-    by blast
+    using of_nat_eq_iff by blast
   then show ?thesis by auto
 qed
 
 lemma sum_of_cubes: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 / 4"
 proof -

 lemma sum_of_cubes_nat: "(\<Sum>k\<le>n::nat. k ^ 3) = (n ^ 2 + n) ^ 2 div 4"
 proof -
   from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
     by (auto simp add: field_simps)
   then have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
-    by blast
+    using of_nat_eq_iff by blast
   then show ?thesis by auto
 qed
 
 end