# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1584903759 0
# Node ID e30dbfa53b0d59b16297232caa5cd11300bd2e73
# Parent  4b1021677f151da54a21c2a0375004f40a948908
new-style Greater lemmas

diff -r 4b1021677f15 -r e30dbfa53b0d src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Mar 22 17:21:16 2020 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Mar 22 19:02:39 2020 +0000
@@ -4367,11 +4367,11 @@
     define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
     assume "\<not>[:c:] dvd b"
     hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
-    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b"
+    have B: "\<And>i. \<not>c dvd coeff b i \<Longrightarrow> i \<le> degree b"
       by (auto intro: le_degree)
     have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B])
     have "i \<le> m" if "\<not>c dvd coeff b i" for i
-      unfolding m_def by (rule Greatest_le_nat[OF that B])
+      unfolding m_def by (metis (mono_tags, lifting) B Greatest_le_nat that)
     hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
 
     have "c dvd coeff a i" for i
diff -r 4b1021677f15 -r e30dbfa53b0d src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Mar 22 17:21:16 2020 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Mar 22 19:02:39 2020 +0000
@@ -286,11 +286,11 @@
     define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
     assume "\<not>[:c:] dvd b"
     hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
-    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b"
+    have B: "\<And>i. \<not>c dvd coeff b i \<Longrightarrow> i \<le> degree b"
       by (auto intro: le_degree)
     have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B])
     have "i \<le> m" if "\<not>c dvd coeff b i" for i
-      unfolding m_def by (rule Greatest_le_nat[OF that B])
+      unfolding m_def by (blast intro!: Greatest_le_nat that B)
     hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
 
     have "c dvd coeff a i" for i