[STATEMENT]
lemma degree_div_mod_smult:
  fixes g::"int poly"
  assumes g: "degree g < j"
  and r: "degree r < d"
  and u: "degree u = d"
  and g1: "g = q * u + smult m r" 
  and q: "q \<noteq> 0" and m_not0: "m \<noteq> 0"
shows "degree q < j - d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have u_not0: "u\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> 0
[PROOF STEP]
using u r
[PROOF STATE]
proof (prove)
using this:
degree u = d
degree r < d

goal (1 subgoal):
 1. u \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<noteq> 0

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have d_uq: "d \<le> degree (u*q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
using u degree_mult_right_le[OF q]
[PROOF STATE]
proof (prove)
using this:
degree u = d
degree ?p \<le> degree (?p * q)

goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> degree (u * q)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have j: "j > degree (q* u + smult m r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * u + Polynomial.smult m r) < j
[PROOF STEP]
using g1 g
[PROOF STATE]
proof (prove)
using this:
g = q * u + Polynomial.smult m r
degree g < j

goal (1 subgoal):
 1. degree (q * u + Polynomial.smult m r) < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (q * u + Polynomial.smult m r) < j

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have "degree (smult m r) < d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult m r) < d
[PROOF STEP]
using degree_smult_eq m_not0 r
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult ?a ?p) = (if ?a = (0::?'a) then 0 else degree ?p)
m \<noteq> 0
degree r < d

goal (1 subgoal):
 1. degree (Polynomial.smult m r) < d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult m r) < d

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult m r) < d

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have "... \<le> degree (u*q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
using d_uq
[PROOF STATE]
proof (prove)
using this:
d \<le> degree (u * q)

goal (1 subgoal):
 1. d \<le> degree (u * q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> degree (u * q)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (Polynomial.smult m r) < degree (u * q)
[PROOF STEP]
have deg_mr_uq: "degree (smult m r) < degree (q*u)"
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult m r) < degree (u * q)

goal (1 subgoal):
 1. degree (Polynomial.smult m r) < degree (q * u)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult m r) < degree (q * u)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have j2: "degree (q* u + smult m r) = degree (q*u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * u + Polynomial.smult m r) = degree (q * u)
[PROOF STEP]
by (rule degree_add_eq_left[OF deg_mr_uq])
[PROOF STATE]
proof (state)
this:
degree (q * u + Polynomial.smult m r) = degree (q * u)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (q * u + Polynomial.smult m r) = degree (q * u)

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
have "... = degree q + degree u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * u) = degree q + degree u
[PROOF STEP]
by (rule degree_mult_eq[OF q u_not0])
[PROOF STATE]
proof (state)
this:
degree (q * u) = degree q + degree u

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (q * u + Polynomial.smult m r) = degree q + degree u
[PROOF STEP]
have "degree q = degree g - degree u"
[PROOF STATE]
proof (prove)
using this:
degree (q * u + Polynomial.smult m r) = degree q + degree u

goal (1 subgoal):
 1. degree q = degree g - degree u
[PROOF STEP]
using g1
[PROOF STATE]
proof (prove)
using this:
degree (q * u + Polynomial.smult m r) = degree q + degree u
g = q * u + Polynomial.smult m r

goal (1 subgoal):
 1. degree q = degree g - degree u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree q = degree g - degree u

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree q = degree g - degree u

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
using j j2 \<open>degree (q * u) = degree q + degree u\<close> u
[PROOF STATE]
proof (prove)
using this:
degree q = degree g - degree u
degree (q * u + Polynomial.smult m r) < j
degree (q * u + Polynomial.smult m r) = degree (q * u)
degree (q * u) = degree q + degree u
degree u = d

goal (1 subgoal):
 1. degree q < j - d
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
degree q < j - d

goal:
No subgoals!
[PROOF STEP]
qed