src/HOL/ex/Sqrt.thy
changeset 61649 268d88ec9087
parent 60690 a9e45c9588c3
child 61762 d50b993b4fb9
     1.1 --- a/src/HOL/ex/Sqrt.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/ex/Sqrt.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -26,7 +26,7 @@
     1.4        by (auto simp add: power2_eq_square)
     1.5      also have "(sqrt p)\<^sup>2 = p" by simp
     1.6      also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
     1.7 -    finally show ?thesis ..
     1.8 +    finally show ?thesis using of_nat_eq_iff by blast
     1.9    qed
    1.10    have "p dvd m \<and> p dvd n"
    1.11    proof
    1.12 @@ -69,7 +69,7 @@
    1.13      by (auto simp add: power2_eq_square)
    1.14    also have "(sqrt p)\<^sup>2 = p" by simp
    1.15    also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
    1.16 -  finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
    1.17 +  finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast
    1.18    then have "p dvd m\<^sup>2" ..
    1.19    with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
    1.20    then obtain k where "m = p * k" ..