equal
deleted
inserted
replaced
284 by (subst (asm) const_poly_dvd_iff) blast |
284 by (subst (asm) const_poly_dvd_iff) blast |
285 { |
285 { |
286 define m where "m = (GREATEST m. \<not>c dvd coeff b m)" |
286 define m where "m = (GREATEST m. \<not>c dvd coeff b m)" |
287 assume "\<not>[:c:] dvd b" |
287 assume "\<not>[:c:] dvd b" |
288 hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast |
288 hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast |
289 have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b" |
289 have B: "\<And>i. \<not>c dvd coeff b i \<Longrightarrow> i \<le> degree b" |
290 by (auto intro: le_degree) |
290 by (auto intro: le_degree) |
291 have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B]) |
291 have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B]) |
292 have "i \<le> m" if "\<not>c dvd coeff b i" for i |
292 have "i \<le> m" if "\<not>c dvd coeff b i" for i |
293 unfolding m_def by (rule Greatest_le_nat[OF that B]) |
293 unfolding m_def by (blast intro!: Greatest_le_nat that B) |
294 hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force |
294 hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force |
295 |
295 |
296 have "c dvd coeff a i" for i |
296 have "c dvd coeff a i" for i |
297 proof (induction i rule: nat_descend_induct[of "degree a"]) |
297 proof (induction i rule: nat_descend_induct[of "degree a"]) |
298 case (base i) |
298 case (base i) |