[STATEMENT]
lemma (in PolynRg) hdeg_p_pOp:"\<lbrakk>p \<in> carrier R; q \<in> carrier R;
      deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d)\<rbrakk> \<Longrightarrow>
      (hdeg_p R S X (Suc d) p) \<plusminus> (hdeg_p R S X (Suc d) q) =
                              hdeg_p R S X (Suc d) (p \<plusminus> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d)\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (cut_tac Ring, frule Ring.ring_is_ag[of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (cut_tac subring, frule subring_Ring[of S])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (frule scf_d_pol[of p "Suc d"], assumption+,
       frule scf_d_pol[of q "Suc d"], assumption+,
        (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); fst (scf_d R S X q (Suc d)) = Suc d; q = polyn_expr R X (Suc d) (scf_d R S X q (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (frule polyn_add1[of "scf_d R S X p (Suc d)" "scf_d R S X q (Suc d)"],
       assumption+,
       rotate_tac -2, drule sym,
       frule aGroup.ag_pOp_closed[of "R" "p" "q"], assumption+,
       frule polyn_deg_add4 [of p q "Suc d"], assumption+,
       rotate_tac -5, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); polyn_expr R X (fst (scf_d R S X p (Suc d))) (scf_d R S X p (Suc d)) \<plusminus> polyn_expr R X (fst (scf_d R S X q (Suc d))) (scf_d R S X q (Suc d)) = polyn_expr R X (max (fst (scf_d R S X p (Suc d))) (fst (scf_d R S X q (Suc d)))) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) \<in> carrier R; deg R S X (polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))))
[PROOF STEP]
apply (rotate_tac -13, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = p \<plusminus> q\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (rotate_tac -1, drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (frule scf_d_pol[of "p \<plusminus> q" "Suc d"], assumption+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); p \<plusminus> q = polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; p \<plusminus> q = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (drule box_equation[of "p \<plusminus> q" "polyn_expr R X (Suc d)
       (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))"
       "polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; p \<plusminus> q = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (
      thin_tac "p \<plusminus> q = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (frule add_cf_pol_coeff[of "scf_d R S X p (Suc d)"
        "scf_d R S X q (Suc d)"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
[PROOF STEP]
apply (cut_tac pol_expr_unique2[of "add_cf S (scf_d R S X p (Suc d))
       (scf_d R S X q (Suc d))" "scf_d R S X (p \<plusminus> q) (Suc d)"],
       simp add:add_cf_len)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); \<forall>j\<le>Suc d. snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) j = snd (scf_d R S X (p \<plusminus> q) (Suc d)) j\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (drule_tac a = "Suc d" in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) (Suc d) = snd (scf_d R S X (p \<plusminus> q) (Suc d)) (Suc d)\<rbrakk> \<Longrightarrow> hdeg_p R S X (Suc d) p \<plusminus> hdeg_p R S X (Suc d) q = hdeg_p R S X (Suc d) (p \<plusminus> q)
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (simp del:npow_suc add:hdeg_p_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) (Suc d) = snd (scf_d R S X (p \<plusminus> q) (Suc d)) (Suc d)\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = snd (scf_d R S X (p \<plusminus> q) (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (rotate_tac -1, drule sym, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); snd (scf_d R S X (p \<plusminus> q) (Suc d)) (Suc d) = snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) (Suc d)\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (subst add_cf_def, simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))); snd (scf_d R S X (p \<plusminus> q) (Suc d)) (Suc d) = snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) (Suc d)\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (snd (scf_d R S X p (Suc d)) (Suc d) \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (thin_tac "polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p",
        thin_tac "polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q",
        thin_tac "polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d))
         (scf_d R S X q (Suc d))) =
          polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d))",
        thin_tac "pol_coeff S (add_cf S (scf_d R S X p (Suc d))
                  (scf_d R S X q (Suc d)))",
        thin_tac "snd (scf_d R S X (p \<plusminus> q) (Suc d)) (Suc d) =
     snd (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) (Suc d)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (snd (scf_d R S X p (Suc d)) (Suc d) \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (frule pol_coeff_mem[of "scf_d R S X p (Suc d)" "Suc d"],
        simp del:npow_suc,
        frule pol_coeff_mem[of "scf_d R S X q (Suc d)" "Suc d"],
        simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S; snd (scf_d R S X q (Suc d)) (Suc d) \<in> carrier S\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (snd (scf_d R S X p (Suc d)) (Suc d) \<plusminus>\<^bsub>S\<^esub> snd (scf_d R S X q (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (simp del:npow_suc add:Subring_pOp_ring_pOp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S; snd (scf_d R S X q (Suc d)) (Suc d) \<in> carrier S\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (snd (scf_d R S X p (Suc d)) (Suc d) \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (frule mem_subring_mem_ring[of S "snd (scf_d R S X p (Suc d)) (Suc d)"],
        assumption,
        frule mem_subring_mem_ring[of S "snd (scf_d R S X q (Suc d)) (Suc d)"],
        assumption,
        cut_tac X_mem_R, frule Ring.npClose[of R X "Suc d"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; fst (scf_d R S X q (Suc d)) = Suc d; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S; snd (scf_d R S X q (Suc d)) (Suc d) \<in> carrier S; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier R; snd (scf_d R S X q (Suc d)) (Suc d) \<in> carrier R; X \<in> carrier R; X^\<^bsup>R Suc d\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (snd (scf_d R S X p (Suc d)) (Suc d) \<plusminus> snd (scf_d R S X q (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 4. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (subst Ring.ring_distrib2[THEN sym], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))
 2. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d))
 3. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (simp add:add_cf_pol_coeff, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; q \<in> carrier R; deg R S X p \<le> an (Suc d); deg R S X q \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); pol_coeff S (scf_d R S X q (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = p; fst (scf_d R S X q (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X q (Suc d)) = q; p \<plusminus> q \<in> carrier R; deg R S X (p \<plusminus> q) \<le> an (Suc d); pol_coeff S (scf_d R S X (p \<plusminus> q) (Suc d)); fst (scf_d R S X (p \<plusminus> q) (Suc d)) = Suc d; polyn_expr R X (Suc d) (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = polyn_expr R X (Suc d) (scf_d R S X (p \<plusminus> q) (Suc d)); pol_coeff S (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d)))\<rbrakk> \<Longrightarrow> fst (add_cf S (scf_d R S X p (Suc d)) (scf_d R S X q (Suc d))) = fst (scf_d R S X (p \<plusminus> q) (Suc d))
[PROOF STEP]
apply (simp add:add_cf_len)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) ldeg_p_mOp:"\<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow>
       -\<^sub>a (ldeg_p R S X d p) = ldeg_p R S X d (-\<^sub>a p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (cut_tac Ring, frule Ring.ring_is_ag[of "R"],
       cut_tac subring, frule subring_Ring[of S],
       frule scf_d_pol[of p "Suc d"], assumption+, (erule conjE)+,
       frule aGroup.ag_mOp_closed[of R p], assumption,
       frule scf_d_pol[of "-\<^sub>a p" "Suc d"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) \<le> an (Suc d)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)) \<and> fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d \<and> -\<^sub>a p = polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d))\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (simp add:deg_minus_eq1, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a p = polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d))\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (frule polyn_minus[of "scf_d R S X p (Suc d)"  "Suc d"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a p = polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)); -\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (drule box_equation[of "-\<^sub>a p" "polyn_expr R X (Suc d)
       (scf_d R S X (-\<^sub>a p) (Suc d))"
       "polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)),
                \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a p = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (rotate_tac 8, drule sym, simp,
       thin_tac "-\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) =
       polyn_expr R X (Suc d)
       (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (frule pol_expr_unique2[of "scf_d R S X (-\<^sub>a p) (Suc d)"
       "(Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> pol_coeff S (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> fst (scf_d R S X (-\<^sub>a p) (Suc d)) = fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); (polyn_expr R X (fst (scf_d R S X (-\<^sub>a p) (Suc d))) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = (\<forall>j\<le>fst (scf_d R S X (-\<^sub>a p) (Suc d)). snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (subst pol_coeff_def, rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); j \<le> Suc d\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> fst (scf_d R S X (-\<^sub>a p) (Suc d)) = fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); (polyn_expr R X (fst (scf_d R S X (-\<^sub>a p) (Suc d))) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = (\<forall>j\<le>fst (scf_d R S X (-\<^sub>a p) (Suc d)). snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of "scf_d R S X p (Suc d)"],
        simp,
        frule Ring.ring_is_ag[of S],
        rule aGroup.ag_mOp_closed[of S], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); (polyn_expr R X (fst (scf_d R S X (-\<^sub>a p) (Suc d))) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = (\<forall>j\<le>fst (scf_d R S X (-\<^sub>a p) (Suc d)). snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) j)\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> -\<^sub>a ldeg_p R S X d p = ldeg_p R S X d (-\<^sub>a p)
[PROOF STEP]
apply (simp add:ldeg_p_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> -\<^sub>a polyn_expr R X d (scf_d R S X p (Suc d)) = polyn_expr R X d (scf_d R S X (-\<^sub>a p) (Suc d))
[PROOF STEP]
apply (subst polyn_minus[of "scf_d R S X p (Suc d)" d], assumption, simp,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) = polyn_expr R X d (scf_d R S X (-\<^sub>a p) (Suc d))
[PROOF STEP]
apply (subst polyn_expr_short[of "(Suc d,
              \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)" d])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> d \<le> fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = polyn_expr R X d (scf_d R S X (-\<^sub>a p) (Suc d))
[PROOF STEP]
apply (subst pol_coeff_def, rule allI, rule impI, simp,
         frule_tac j = j in pol_coeff_mem[of "scf_d R S X p (Suc d)"],
         simp,
         frule Ring.ring_is_ag[of S],
         rule aGroup.ag_mOp_closed[of S], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = polyn_expr R X d (scf_d R S X (-\<^sub>a p) (Suc d))
[PROOF STEP]
apply (subst polyn_expr_short[of "scf_d R S X (-\<^sub>a p) (Suc d)" d],
          assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> polyn_expr R X d (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = polyn_expr R X d (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
[PROOF STEP]
apply (cut_tac pol_expr_unique2[of "(d, snd (Suc d,
                \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j))"
                "(d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j; (polyn_expr R X (fst (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j))) (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = polyn_expr R X (fst (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))) (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))) = (\<forall>j\<le>fst (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)). snd (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) j = snd (d, snd (scf_d R S X (-\<^sub>a p) (Suc d))) j)\<rbrakk> \<Longrightarrow> polyn_expr R X d (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = polyn_expr R X d (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j))
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
 4. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> fst (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = fst (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
[PROOF STEP]
apply (thin_tac "p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))",
        thin_tac "polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) =
     polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)",
        simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j))
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> fst (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = fst (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
[PROOF STEP]
apply (subst pol_coeff_def, rule allI, rule impI, simp,
         frule Ring.ring_is_ag[of S], rule aGroup.ag_mOp_closed, assumption,
         simp add:pol_coeff_mem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> pol_coeff S (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> fst (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = fst (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
[PROOF STEP]
apply (subst pol_coeff_def, rule allI, rule impI, simp,
         frule Ring.ring_is_ag[of S], rule aGroup.ag_mOp_closed, assumption,
         simp add:pol_coeff_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> fst (d, snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = fst (d, snd (scf_d R S X (-\<^sub>a p) (Suc d)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) hdeg_p_mOp:"\<lbrakk>p \<in> carrier R;deg R S X p \<le> an (Suc d)\<rbrakk>
  \<Longrightarrow> -\<^sub>a (hdeg_p R S X (Suc d) p) = hdeg_p R S X (Suc d) (-\<^sub>a p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (cut_tac Ring, frule Ring.ring_is_ag[of "R"],
       cut_tac subring, frule subring_Ring[of S],
       frule scf_d_pol[of p "Suc d"], assumption+, (erule conjE)+,
       frule aGroup.ag_mOp_closed[of R p], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (
       frule scf_d_pol[of "-\<^sub>a p" "Suc d"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R\<rbrakk> \<Longrightarrow> deg R S X (-\<^sub>a p) \<le> an (Suc d)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)) \<and> fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d \<and> -\<^sub>a p = polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d))\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (simp add:deg_minus_eq1, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a p = polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d))\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (frule polyn_minus[of "scf_d R S X p (Suc d)"  "Suc d"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a p = polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)); -\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (drule box_equation[of "-\<^sub>a p" "polyn_expr R X (Suc d)
       (scf_d R S X (-\<^sub>a p) (Suc d))"
       "polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)),
                \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a p = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; -\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (rotate_tac 8, drule sym, simp,
       thin_tac "-\<^sub>a polyn_expr R X (Suc d) (scf_d R S X p (Suc d)) =
       polyn_expr R X (Suc d)
       (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (fst (scf_d R S X p (Suc d)), \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (frule pol_expr_unique2[of "scf_d R S X (-\<^sub>a p) (Suc d)"
       "(Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> pol_coeff S (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> fst (scf_d R S X (-\<^sub>a p) (Suc d)) = fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); (polyn_expr R X (fst (scf_d R S X (-\<^sub>a p) (Suc d))) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = (\<forall>j\<le>fst (scf_d R S X (-\<^sub>a p) (Suc d)). snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (subst pol_coeff_def, rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); j \<le> Suc d\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j \<in> carrier S
 2. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)\<rbrakk> \<Longrightarrow> fst (scf_d R S X (-\<^sub>a p) (Suc d)) = fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)
 3. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); (polyn_expr R X (fst (scf_d R S X (-\<^sub>a p) (Suc d))) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = (\<forall>j\<le>fst (scf_d R S X (-\<^sub>a p) (Suc d)). snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (frule_tac j = j in pol_coeff_mem[of "scf_d R S X p (Suc d)"],
        simp,
        frule Ring.ring_is_ag[of S],
        rule aGroup.ag_mOp_closed[of S], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); (polyn_expr R X (fst (scf_d R S X (-\<^sub>a p) (Suc d))) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (fst (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)) = (\<forall>j\<le>fst (scf_d R S X (-\<^sub>a p) (Suc d)). snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = snd (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j) j)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); \<forall>j\<le>Suc d. snd (scf_d R S X (-\<^sub>a p) (Suc d)) j = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (drule_tac a = "Suc d" in forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); snd (scf_d R S X (-\<^sub>a p) (Suc d)) (Suc d) = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)\<rbrakk> \<Longrightarrow> -\<^sub>a hdeg_p R S X (Suc d) p = hdeg_p R S X (Suc d) (-\<^sub>a p)
[PROOF STEP]
apply (simp del:npow_suc add:hdeg_p_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d)); -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) = polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j); snd (scf_d R S X (-\<^sub>a p) (Suc d)) (Suc d) = -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)\<rbrakk> \<Longrightarrow> -\<^sub>a snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (-\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
[PROOF STEP]
apply (thin_tac "p = polyn_expr R X (Suc d) (scf_d R S X p (Suc d))",
        thin_tac "polyn_expr R X (Suc d) (scf_d R S X (-\<^sub>a p) (Suc d)) =
     polyn_expr R X (Suc d) (Suc d, \<lambda>j. -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) j)",
        thin_tac "snd (scf_d R S X (-\<^sub>a p) (Suc d)) (Suc d) =
     -\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d\<rbrakk> \<Longrightarrow> -\<^sub>a snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (-\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
[PROOF STEP]
apply (frule pol_coeff_mem[of "scf_d R S X p (Suc d)" "Suc d"], simp,
        frule mem_subring_mem_ring[of S "snd (scf_d R S X p (Suc d)) (Suc d)"],
        assumption+,
        frule Ring.npClose[of R X "Suc d"], simp add:X_mem_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier R; X^\<^bsup>R Suc d\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a snd (scf_d R S X p (Suc d)) (Suc d) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (-\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
[PROOF STEP]
apply (subst Ring.ring_inv1_1[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; deg R S X p \<le> an (Suc d); Ring R; aGroup R; Subring R S; Ring S; pol_coeff S (scf_d R S X p (Suc d)); fst (scf_d R S X p (Suc d)) = Suc d; -\<^sub>a p \<in> carrier R; pol_coeff S (scf_d R S X (-\<^sub>a p) (Suc d)); fst (scf_d R S X (-\<^sub>a p) (Suc d)) = Suc d; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier S; snd (scf_d R S X p (Suc d)) (Suc d) \<in> carrier R; X^\<^bsup>R Suc d\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> (-\<^sub>a snd (scf_d R S X p (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup> = (-\<^sub>a\<^bsub>S\<^esub> snd (scf_d R S X p (Suc d)) (Suc d)) \<cdot>\<^sub>r X^\<^bsup>R Suc d\<^esup>
[PROOF STEP]
apply (simp del:npow_suc add:Subring_minus_ring_minus)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done