src/HOL/Polynomial.thy
 changeset 29453 de4f26f59135 parent 29451 5f0cb3fa530d child 29454 b0f586f38dd7
```     1.1 --- a/src/HOL/Polynomial.thy	Sun Jan 11 21:50:05 2009 +0100
1.2 +++ b/src/HOL/Polynomial.thy	Mon Jan 12 08:15:07 2009 -0800
1.3 @@ -319,6 +319,10 @@
1.4  lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"
1.5    by (rule degree_le, auto simp add: coeff_eq_0)
1.6
1.8 +  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
1.9 +  by (auto intro: le_less_trans degree_add_le)
1.10 +
1.12    "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
1.13    apply (cases "q = 0", simp)
1.14 @@ -341,6 +345,10 @@
1.15    using degree_add_le [where p=p and q="-q"]
1.17
1.18 +lemma degree_diff_less:
1.19 +  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
1.20 +  by (auto intro: le_less_trans degree_diff_le)
1.21 +
1.22  lemma add_monom: "monom a n + monom b n = monom (a + b) n"
1.23    by (rule poly_ext) simp
1.24
1.25 @@ -762,7 +770,7 @@
1.26    from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"