# HG changeset patch
# User huffman
# Date 1235402393 28800
# Node ID 4eecd8b9b6cf3ec0578dde863bc15b746b9664e5
# Parent  be46f437ace23889f399871d4615577b1cad068c
add lemmas poly_{div,mod}_minus_{left,right}

diff -r be46f437ace2 -r 4eecd8b9b6cf src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Feb 23 06:51:26 2009 -0800
+++ b/src/HOL/Library/Polynomial.thy	Mon Feb 23 07:19:53 2009 -0800
@@ -1020,6 +1020,16 @@
 lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
   by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
 
+lemma poly_div_minus_left [simp]:
+  fixes x y :: "'a::field poly"
+  shows "(- x) div y = - (x div y)"
+  using div_smult_left [of "- 1::'a"] by simp
+
+lemma poly_mod_minus_left [simp]:
+  fixes x y :: "'a::field poly"
+  shows "(- x) mod y = - (x mod y)"
+  using mod_smult_left [of "- 1::'a"] by simp
+
 lemma pdivmod_rel_smult_right:
   "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
     \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
@@ -1032,6 +1042,17 @@
 lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
   by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
 
+lemma poly_div_minus_right [simp]:
+  fixes x y :: "'a::field poly"
+  shows "x div (- y) = - (x div y)"
+  using div_smult_right [of "- 1::'a"]
+  by (simp add: nonzero_inverse_minus_eq)
+
+lemma poly_mod_minus_right [simp]:
+  fixes x y :: "'a::field poly"
+  shows "x mod (- y) = x mod y"
+  using mod_smult_right [of "- 1::'a"] by simp
+
 lemma pdivmod_rel_mult:
   "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
     \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"