# HG changeset patch
# User huffman
# Date 1231776907 28800
# Node ID de4f26f59135c0f0d4f1b5a02e359a5865580d68
# Parent  b81ae415873d7f3c85f68aef8e23e687ca8e95d9
add lemmas degree_{add,diff}_less

diff -r b81ae415873d -r de4f26f59135 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Sun Jan 11 21:50:05 2009 +0100
+++ b/src/HOL/Polynomial.thy	Mon Jan 12 08:15:07 2009 -0800
@@ -319,6 +319,10 @@
 lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"
   by (rule degree_le, auto simp add: coeff_eq_0)
 
+lemma degree_add_less:
+  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
+  by (auto intro: le_less_trans degree_add_le)
+
 lemma degree_add_eq_right:
   "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
   apply (cases "q = 0", simp)
@@ -341,6 +345,10 @@
   using degree_add_le [where p=p and q="-q"]
   by (simp add: diff_minus)
 
+lemma degree_diff_less:
+  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
+  by (auto intro: le_less_trans degree_diff_le)
+
 lemma add_monom: "monom a n + monom b n = monom (a + b) n"
   by (rule poly_ext) simp
 
@@ -762,7 +770,7 @@
   from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
     by (simp add: ring_simps)
   from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
-    by (auto intro: le_less_trans [OF degree_diff_le])
+    by (auto intro: degree_diff_less)
 
   show "q1 = q2 \<and> r1 = r2"
   proof (rule ccontr)