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" ..
```