src/HOL/ex/Sum_of_Powers.thy
changeset 61649 268d88ec9087
parent 61609 77b453bd616f
child 61694 6571c78c9667
     1.1 --- a/src/HOL/ex/Sum_of_Powers.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/ex/Sum_of_Powers.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -175,7 +175,7 @@
     1.4    from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
     1.5      by (auto simp add: field_simps)
     1.6    then have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
     1.7 -    by blast
     1.8 +    using of_nat_eq_iff by blast
     1.9    then show ?thesis by auto
    1.10  qed
    1.11  
    1.12 @@ -197,7 +197,7 @@
    1.13    from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
    1.14      by (auto simp add: field_simps)
    1.15    then have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
    1.16 -    by blast
    1.17 +    using of_nat_eq_iff by blast
    1.18    then show ?thesis by auto
    1.19  qed
    1.20