Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Discrete.thy
changeset 70365 4df0628e8545
parent 69064 5840724b1d71 
--- a/src/HOL/Library/Discrete.thy	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Library/Discrete.thy	Wed Jul 17 14:02:42 2019 +0100
@@ -332,7 +332,8 @@
     have "(Discrete.sqrt n)^2 < m^2" by linarith
   with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
   from m_def Suc_sqrt_power2_gt[of "n"]
-    have "m^2 \<le> (Suc(Discrete.sqrt n))^2" by simp
+    have "m^2 \<le> (Suc(Discrete.sqrt n))^2"
+      by linarith
   with power2_nat_le_eq_le have "m \<le> Suc (Discrete.sqrt n)" by blast
   with lt_m have "m = Suc (Discrete.sqrt n)" by simp
   with lhs m_def show ?thesis by fastforce
isabelle