[STATEMENT]
lemma (in PolynRg) pol_expr_edeg:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> (an d)\<rbrakk> \<Longrightarrow>
       \<exists>f. (pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (subgoal_tac "pol_coeff S (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> fst (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>) = d \<and>
              p = polyn_expr R X d (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)", blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>) \<and> fst (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>) = d \<and> p = polyn_expr R X d (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> fst (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>) = d \<and> p = polyn_expr R X d (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (simp add:pol_coeff_def, cut_tac Ring.ring_zero[of S], simp,
        cut_tac subring, simp add:subring_Ring)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> fst (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>) = d \<and> p = polyn_expr R X d (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (cut_tac coeff_0_pol_0[of "(d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)" d], simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (simp add:pol_coeff_def, cut_tac Ring.ring_zero[of S], simp,
        cut_tac subring, simp add:subring_Ring)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p = \<zero>\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (frule s_cf_expr[of p], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f
[PROOF STEP]
apply (simp add:deg_def na_an, simp add:ale_natle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg_n R S X p \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<exists>b. pol_coeff S (d, b) \<and> p = polyn_expr R X d (d, b)
[PROOF STEP]
apply (simp add:s_cf_deg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> \<exists>b. pol_coeff S (d, b) \<and> p = polyn_expr R X d (d, b)
[PROOF STEP]
apply (subgoal_tac "pol_coeff S (d, \<lambda>j. (if j \<le> (fst (s_cf R S X p)) then
         (snd (s_cf R S X p) j) else \<zero>\<^bsub>S\<^esub>)) \<and>
         p = polyn_expr R X d (d, \<lambda>j. (if j \<le> (fst (s_cf R S X p)) then
         (snd (s_cf R S X p) j) else \<zero>\<^bsub>S\<^esub>))", blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<and> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (simp add:pol_coeff_def, rule allI, rule impI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; \<forall>j\<le>fst (s_cf R S X p). snd (s_cf R S X p) j \<in> carrier S; p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; \<not> j \<le> fst (s_cf R S X p); j \<le> d\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>S\<^esub> \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (cut_tac subring, simp add:subring_Ring, simp add:subring_Ring[of S]
         Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (case_tac "fst (s_cf R S X p) = d", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> d then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (subst polyn_exprs_eq[of "(d, \<lambda>j. if j \<le> d then snd (s_cf R S X p) j
         else \<zero>\<^bsub>S\<^esub>)" "s_cf R S X p" d])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> d then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> d \<le> min (fst (d, \<lambda>j. if j \<le> d then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)) (fst (s_cf R S X p))
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> \<forall>j\<le>d. snd (d, \<lambda>j. if j \<le> d then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = snd (s_cf R S X p) j
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (s_cf R S X p)
 6. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (simp add:pol_coeff_def, cut_tac Ring.ring_zero[of S], simp,
          cut_tac subring, simp add:subring_Ring, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> \<forall>j\<le>d. snd (d, \<lambda>j. if j \<le> d then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = snd (s_cf R S X p) j
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X d (s_cf R S X p); snd (s_cf R S X p) d \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) = d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (s_cf R S X p)
 3. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI, simp, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; fst (s_cf R S X p) \<le> d; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (drule noteq_le_less[of "fst (s_cf R S X p)" d], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (cut_tac polyn_n_m1[of "(d, \<lambda>j. if j \<le> fst (s_cf R S X p) then
        snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)" "fst (s_cf R S X p)" d], simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (cut_tac higher_part_zero[of "(d, \<lambda>j. if j \<le> fst (s_cf R S X p) then
     snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)" "fst (s_cf R S X p)"], simp,
     thin_tac "polyn_expr R X d
      (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) =
     polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p)
      then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<zero>",
     thin_tac "\<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j
                else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) (Suc (fst (s_cf R S X p))) d = \<zero>")
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<zero>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 7. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (subst polyn_exprs_eq[of "(d, \<lambda>j. if j \<le> fst (s_cf R S X p) then
       snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)" "s_cf R S X p" "fst (s_cf R S X p)"])
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (s_cf R S X p)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) \<le> min (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)) (fst (s_cf R S X p))
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X p). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = snd (s_cf R S X p) j
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<plusminus> \<zero>
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 7. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 8. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 9. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 10. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
A total of 11 subgoals...
[PROOF STEP]
apply (simp add:pol_coeff_def, rule allI, rule impI, rule impI,
         cut_tac subring, simp add:subring_Ring, simp add:subring_Ring[of S]
         Ring.ring_zero, assumption+)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) \<le> min (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)) (fst (s_cf R S X p))
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X p). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = snd (s_cf R S X p) j
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<plusminus> \<zero>
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 7. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 8. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 9. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X p). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = snd (s_cf R S X p) j
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<plusminus> \<zero>
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 7. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 8. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p) \<plusminus> \<zero>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 7. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (frule polyn_mem[of "s_cf R S X p" "fst (s_cf R S X p)"], simp+)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> p = p \<plusminus> \<zero>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 7. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (cut_tac ring_is_ag, simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 6. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (simp add:pol_coeff_def, rule allI, rule impI, rule impI,
         cut_tac subring, simp add:subring_Ring, simp add:subring_Ring[of S]
         Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 5. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) < d; polyn_expr R X d (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) = polyn_expr R X (fst (s_cf R S X p)) (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<plusminus> \<Sigma>\<^sub>f R (\<lambda>j. (if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) \<cdot>\<^sub>r X^\<^bsup>R j\<^esup>) Suc (fst (s_cf R S X p)) d\<rbrakk> \<Longrightarrow> \<forall>j\<in>nset (Suc (fst (s_cf R S X p))) (fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)). snd (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>) j = \<zero>\<^bsub>S\<^esub>
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 4. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule ballI, simp add:nset_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> pol_coeff S (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 3. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (simp add:pol_coeff_def, rule allI, rule impI, rule impI,
         cut_tac subring, simp add:subring_Ring, simp add:subring_Ring[of S]
         Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> fst (s_cf R S X p) < d
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S (s_cf R S X p); p = polyn_expr R X (fst (s_cf R S X p)) (s_cf R S X p); snd (s_cf R S X p) (fst (s_cf R S X p)) \<noteq> \<zero>\<^bsub>S\<^esub>; fst (s_cf R S X p) \<noteq> d; fst (s_cf R S X p) < d\<rbrakk> \<Longrightarrow> d \<le> fst (d, \<lambda>j. if j \<le> fst (s_cf R S X p) then snd (s_cf R S X p) j else \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) cf_scf:"\<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k c \<noteq> \<zero>\<rbrakk>
    \<Longrightarrow>  \<forall>j \<le> fst (s_cf R S X (polyn_expr R X k c)).
              snd (s_cf R S X (polyn_expr R X k c)) j = snd c j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k c \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X (polyn_expr R X k c)). snd (s_cf R S X (polyn_expr R X k c)) j = snd c j
[PROOF STEP]
apply (frule polyn_mem[of c k], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k c \<noteq> \<zero>; polyn_expr R X k c \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>j\<le>fst (s_cf R S X (polyn_expr R X k c)). snd (s_cf R S X (polyn_expr R X k c)) j = snd c j
[PROOF STEP]
apply (simp add:polyn_expr_short[of c k],
       rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> snd (s_cf R S X (polyn_expr R X k (k, snd c))) j = snd c j
[PROOF STEP]
apply (cut_tac pol_deg_le_n1[of "polyn_expr R X k c" c k],
       frule s_cf_expr0[of "polyn_expr R X k (k, snd c)"], erule conjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c))); deg_n R S X (polyn_expr R X k c) \<le> k; pol_coeff S (s_cf R S X (polyn_expr R X k (k, snd c))); polyn_expr R X k (k, snd c) = polyn_expr R X (fst (s_cf R S X (polyn_expr R X k (k, snd c)))) (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> snd (s_cf R S X (polyn_expr R X k (k, snd c))) j = snd c j
 2. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c \<in> carrier R
 3. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> pol_coeff S c
 4. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> k \<le> fst c
 5. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c = polyn_expr R X k c
[PROOF STEP]
apply (rotate_tac -1, drule sym)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c))); deg_n R S X (polyn_expr R X k c) \<le> k; pol_coeff S (s_cf R S X (polyn_expr R X k (k, snd c))); polyn_expr R X (fst (s_cf R S X (polyn_expr R X k (k, snd c)))) (s_cf R S X (polyn_expr R X k (k, snd c))) = polyn_expr R X k (k, snd c)\<rbrakk> \<Longrightarrow> snd (s_cf R S X (polyn_expr R X k (k, snd c))) j = snd c j
 2. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c \<in> carrier R
 3. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> pol_coeff S c
 4. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> k \<le> fst c
 5. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c = polyn_expr R X k c
[PROOF STEP]
apply (case_tac "fst (s_cf R S X (polyn_expr R X k (k, snd c))) = k",
       simp,
       cut_tac c = "s_cf R S X (polyn_expr R X k (k, snd c))" and
       d = "(k, snd c)" in pol_expr_unique2,
       simp add:s_cf_pol_coeff, simp add:split_pol_coeff, simp,
        simp, simp add:polyn_expr_short[THEN sym, of c k])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k c \<noteq> \<zero>; polyn_expr R X k c \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k c)); deg_n R S X (polyn_expr R X k c) \<le> k; pol_coeff S (s_cf R S X (polyn_expr R X k c)); polyn_expr R X (fst (s_cf R S X (polyn_expr R X k c))) (s_cf R S X (polyn_expr R X k c)) = polyn_expr R X k c; fst (s_cf R S X (polyn_expr R X k c)) \<noteq> k\<rbrakk> \<Longrightarrow> snd (s_cf R S X (polyn_expr R X k c)) j = snd c j
 2. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c \<in> carrier R
 3. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> pol_coeff S c
 4. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> k \<le> fst c
 5. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c = polyn_expr R X k c
[PROOF STEP]
apply (simp add:s_cf_deg[of "polyn_expr R X k c"],
        drule noteq_le_less[of "fst (s_cf R S X (polyn_expr R X k c))" k],
        assumption)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k c \<noteq> \<zero>; polyn_expr R X k c \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k c)); pol_coeff S (s_cf R S X (polyn_expr R X k c)); polyn_expr R X (fst (s_cf R S X (polyn_expr R X k c))) (s_cf R S X (polyn_expr R X k c)) = polyn_expr R X k c; fst (s_cf R S X (polyn_expr R X k c)) \<noteq> k; fst (s_cf R S X (polyn_expr R X k c)) < k\<rbrakk> \<Longrightarrow> snd (s_cf R S X (polyn_expr R X k c)) j = snd c j
 2. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c \<in> carrier R
 3. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> pol_coeff S c
 4. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> k \<le> fst c
 5. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c = polyn_expr R X k c
[PROOF STEP]
apply (frule pol_expr_unique3[of "s_cf R S X (polyn_expr R X k c)"
         "(k, snd c)"], simp add:split_pol_coeff, simp,
        simp add:polyn_expr_short[THEN sym, of c k])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c \<in> carrier R
 2. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> pol_coeff S c
 3. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> k \<le> fst c
 4. \<And>j. \<lbrakk>pol_coeff S c; k \<le> fst c; polyn_expr R X k (k, snd c) \<noteq> \<zero>; polyn_expr R X k (k, snd c) \<in> carrier R; j \<le> fst (s_cf R S X (polyn_expr R X k (k, snd c)))\<rbrakk> \<Longrightarrow> polyn_expr R X k c = polyn_expr R X k c
[PROOF STEP]
apply (simp add:polyn_expr_short[THEN sym, of c k], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) scf_d_polTr:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow>
           scf_cond R S X p d (scf_d R S X p d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow> scf_cond R S X p d (scf_d R S X p d)
[PROOF STEP]
apply (simp add:scf_d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow> scf_cond R S X p d (SOME f. scf_cond R S X p d f)
[PROOF STEP]
apply (rule_tac P = "scf_cond R S X p d" in someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow> \<exists>a. scf_cond R S X p d a
 2. \<And>x. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; scf_cond R S X p d x\<rbrakk> \<Longrightarrow> scf_cond R S X p d x
[PROOF STEP]
apply (frule pol_expr_edeg[of "p" "d"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; \<exists>f. pol_coeff S f \<and> fst f = d \<and> p = polyn_expr R X d f\<rbrakk> \<Longrightarrow> \<exists>a. scf_cond R S X p d a
 2. \<And>x. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; scf_cond R S X p d x\<rbrakk> \<Longrightarrow> scf_cond R S X p d x
[PROOF STEP]
apply (simp add:scf_cond_def, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) scf_d_pol:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow>
      pol_coeff S (scf_d R S X p d) \<and> fst (scf_d R S X p d) = d \<and>
       p = polyn_expr R X d (scf_d R S X p d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X p d) \<and> fst (scf_d R S X p d) = d \<and> p = polyn_expr R X d (scf_d R S X p d)
[PROOF STEP]
apply (frule scf_d_polTr[of "p" "d"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an d; scf_cond R S X p d (scf_d R S X p d)\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X p d) \<and> fst (scf_d R S X p d) = d \<and> p = polyn_expr R X d (scf_d R S X p d)
[PROOF STEP]
apply (simp add:scf_cond_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pol_expr_of_X:
       "X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))
[PROOF STEP]
apply (cut_tac X_mem_R, cut_tac subring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; Subring R S\<rbrakk> \<Longrightarrow> X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))
[PROOF STEP]
apply (cut_tac X_to_d[of "Suc 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; Subring R S; X^\<^bsup>R Suc 0\<^esup> = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))
[PROOF STEP]
apply (simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) deg_n_of_X:"deg_n R S X X = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deg_n R S X X = Suc 0
[PROOF STEP]
apply (cut_tac X_mem_R, cut_tac polyn_ring_S_nonzero,
       cut_tac subring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S\<rbrakk> \<Longrightarrow> deg_n R S X X = Suc 0
[PROOF STEP]
apply (cut_tac pol_expr_of_X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> deg_n R S X X = Suc 0
[PROOF STEP]
apply (cut_tac special_cf_pol_coeff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S)\<rbrakk> \<Longrightarrow> deg_n R S X X = Suc 0
[PROOF STEP]
apply (frule ext_cf_pol_coeff[of "C\<^sub>0 S" "Suc 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> deg_n R S X X = Suc 0
[PROOF STEP]
apply (frule pol_deg_eq_c_max[of X "ext_cf S (Suc 0) (C\<^sub>0 S)"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> X = polyn_expr R X (fst (ext_cf S (Suc 0) (C\<^sub>0 S))) (ext_cf S (Suc 0) (C\<^sub>0 S))
 2. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); deg_n R S X X = c_max S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> deg_n R S X X = Suc 0
[PROOF STEP]
apply (simp add:ext_cf_len special_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> carrier R; 1\<^sub>r\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>; Subring R S; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); deg_n R S X X = c_max S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> deg_n R S X X = Suc 0
[PROOF STEP]
apply (simp add:c_max_ext_special_cf)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) pol_X:"cf_sol R S X X c \<Longrightarrow>
              snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_sol R S X X c \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:cf_sol_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac pol_expr_of_X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac special_cf_pol_coeff,
               frule ext_cf_pol_coeff[of "C\<^sub>0 S" "Suc 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac X_mem_R, cut_tac polyn_ring_X_nonzero,
       cut_tac subring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule pol_deg_le_n[of X c], assumption+, simp add:deg_n_of_X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (case_tac "fst c = Suc 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c = Suc 0\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
 2. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule box_equation[of X "polyn_expr R X (Suc 0)
       (ext_cf S (Suc 0) (C\<^sub>0 S))" "polyn_expr R X (fst c) c"], assumption+,
       thin_tac "X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S))",
       thin_tac "X = polyn_expr R X (fst c) c")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pol_coeff S c; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c = Suc 0; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
 2. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (cut_tac pol_expr_unique2[of "ext_cf S (Suc 0) (C\<^sub>0 S)" c],
       simp, simp add:ext_cf_len special_cf_len, rule conjI,
       drule_tac a = 0 in forall_spec, simp,
       simp add:ext_special_cf_lo_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>pol_coeff S c; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; fst c = Suc 0; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (Suc 0) c; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd c j\<rbrakk> \<Longrightarrow> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
 2. \<lbrakk>pol_coeff S c; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c = Suc 0; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))
 3. \<lbrakk>pol_coeff S c; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c = Suc 0; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> pol_coeff S c
 4. \<lbrakk>pol_coeff S c; pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c = Suc 0; polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)) = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> fst (ext_cf S (Suc 0) (C\<^sub>0 S)) = fst c
 5. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply( drule_tac a = "Suc 0" in forall_spec, simp,
       simp add:ext_special_cf_hi, assumption+,
       simp add:ext_cf_len special_cf_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule noteq_le_less[of "Suc 0" "fst c"],rule not_sym, assumption,
       cut_tac pol_expr_unique3[of "ext_cf S (Suc 0) (C\<^sub>0 S)" c],
       simp add:ext_cf_len special_cf_len,
       erule conjE,
       thin_tac "\<forall>j\<in>nset (Suc (Suc 0)) (fst c). snd c j = \<zero>\<^bsub>S\<^esub>")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 < fst c; \<forall>j\<le>Suc 0. snd (ext_cf S (Suc 0) (C\<^sub>0 S)) j = snd c j\<rbrakk> \<Longrightarrow> snd c 0 = \<zero>\<^bsub>S\<^esub> \<and> snd c (Suc 0) = 1\<^sub>r\<^bsub>S\<^esub>
 2. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0; Suc 0 < fst c\<rbrakk> \<Longrightarrow> pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S))
 3. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0; Suc 0 < fst c\<rbrakk> \<Longrightarrow> pol_coeff S c
 4. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0; Suc 0 < fst c\<rbrakk> \<Longrightarrow> fst (ext_cf S (Suc 0) (C\<^sub>0 S)) < fst c
[PROOF STEP]
apply (rule conjI,
        drule_tac a = 0 in forall_spec, simp,
        simp add:ext_special_cf_lo_zero,
        drule_tac a = "Suc 0" in forall_spec, simp,
        simp add:ext_special_cf_hi,
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pol_coeff S c; X = polyn_expr R X (fst c) c; X = polyn_expr R X (Suc 0) (ext_cf S (Suc 0) (C\<^sub>0 S)); pol_coeff S (C\<^sub>0 S); pol_coeff S (ext_cf S (Suc 0) (C\<^sub>0 S)); X \<in> carrier R; X \<noteq> \<zero>; Subring R S; Suc 0 \<le> fst c; fst c \<noteq> Suc 0; Suc 0 < fst c\<rbrakk> \<Longrightarrow> fst (ext_cf S (Suc 0) (C\<^sub>0 S)) < fst c
[PROOF STEP]
apply (simp add:ext_cf_len special_cf_len)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done