[STATEMENT]
lemma (in PolynRg) s_cf_pol_coeff:"p \<in> carrier R \<Longrightarrow>
                         pol_coeff S (s_cf R S X p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> pol_coeff S (s_cf R S X p)
[PROOF STEP]
apply (simp add:s_cf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier R \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<zero> \<in> carrier R; p = \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)
 2. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring, 
             simp add:pol_coeff_def Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> (p = \<zero> \<longrightarrow> pol_coeff S (0, \<lambda>j. \<zero>\<^bsub>S\<^esub>)) \<and> (p \<noteq> \<zero> \<longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> pol_coeff S (SOME c. pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>)
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (frule ex_polyn_expr[of p], erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (frule_tac c = c in coeff_max_bddTr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (frule_tac c = c and n = "c_max S c" in pol_coeff_le, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>a. pol_coeff S a \<and> p = polyn_expr R X (fst a) a \<and> snd a (fst a) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (subgoal_tac "p = polyn_expr R X (fst (c_max S c, snd c))
                                                  (c_max S c, snd c) \<and>
                     snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>",
        blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> p = polyn_expr R X (fst (c_max S c, snd c)) (c_max S c, snd c) \<and> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (rule conjI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) (c_max S c, snd c)
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (subst polyn_expr_short[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> polyn_expr R X (fst c) c = polyn_expr R X (c_max S c) c
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 3. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (simp add:polyn_c_max)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd (c_max S c, snd c) (fst (c_max S c, snd c)) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> snd c (c_max S c) \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (rule coeff_max_nonzeroTr, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; polyn_expr R X (fst c) c \<noteq> \<zero>; pol_coeff S c; p = polyn_expr R X (fst c) c; c_max S c \<le> fst c; pol_coeff S (c_max S c, snd c)\<rbrakk> \<Longrightarrow> \<exists>j\<le>fst c. snd c j \<noteq> \<zero>\<^bsub>S\<^esub>
 2. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply (simp add:coeff_0_pol_0[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>p \<in> carrier R; p \<noteq> \<zero>; pol_coeff S c \<and> p = polyn_expr R X (fst c) c \<and> snd c (fst c) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> pol_coeff S c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done