--- a/src/HOL/Library/Polynomial.thy Wed Apr 15 15:52:37 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy Thu Apr 16 10:11:34 2009 +0200
@@ -987,6 +987,30 @@
by (simp add: pdivmod_rel_def left_distrib)
thus "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
+next
+ fix x y z :: "'a poly"
+ assume "x \<noteq> 0"
+ show "(x * y) div (x * z) = y div z"
+ proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
+ have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
+ by (rule pdivmod_rel_by_0)
+ then have [simp]: "\<And>x::'a poly. x div 0 = 0"
+ by (rule div_poly_eq)
+ have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
+ by (rule pdivmod_rel_0)
+ then have [simp]: "\<And>x::'a poly. 0 div x = 0"
+ by (rule div_poly_eq)
+ case False then show ?thesis by auto
+ next
+ case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
+ with `x \<noteq> 0`
+ have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
+ by (auto simp add: pdivmod_rel_def algebra_simps)
+ (rule classical, simp add: degree_mult_eq)
+ moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
+ ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
+ then show ?thesis by (simp add: div_poly_eq)
+ qed
qed
end