[STATEMENT]
lemma (in PolynRg) divisionTr1:"\<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>;
      0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f\<rbrakk>
      \<Longrightarrow>
      f \<plusminus> -\<^sub>a ((lcf R S X f) \<cdot>\<^sub>r\<^bsub>S\<^esub> ((lcf R S X g)\<^bsup>\<hyphen> S\<^esup>) \<cdot>\<^sub>r
                     (X^\<^bsup>R ((deg_n R S X f) - (deg_n R S X g))\<^esup>) \<cdot>\<^sub>r g) = \<zero> \<or>
      deg_n R S X (f \<plusminus> -\<^sub>a ((lcf R S X f) \<cdot>\<^sub>r\<^bsub>S\<^esub> ((lcf R S X g)\<^bsup>\<hyphen> S\<^esup>) \<cdot>\<^sub>r
                 (X^\<^bsup>R ((deg_n R S X f) - (deg_n R S X g))\<^esup>) \<cdot>\<^sub>r g)) < deg_n R S X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac subring,
       frule Corps.field_is_idom[of "S"],
       frule subring_Ring,
       cut_tac subring,
       cut_tac polyn_ring_X_nonzero,
       cut_tac X_mem_R,
       cut_tac polyn_ring_integral, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; aGroup R; Idomain R; Ring S; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f
[PROOF STEP]
apply (frule npClose[of X "deg_n R S X f - deg_n R S X g"],
       frule_tac Idomain.idom_potent_nonzero[of R X
                "fst (s_cf R S X f) - fst (s_cf R S X g)"], assumption+,
       frule s_cf_expr[of f], assumption+, (erule conjE)+,
       frule s_cf_expr[of g], assumption+, (erule conjE)+,
       simp add:s_cf_deg, simp add:lcf_val[THEN sym],
       frule Corps.invf_closed1[of S "lcf R S X g"], simp, simp add:lcf_mem,
       frule lcf_mem[of f], simp,
       frule subring_Ring, frule Ring.ring_is_ag[of S], (erule conjE)+,
       frule_tac x = "lcf R S X f" and y = "lcf R S X g\<^bsup>\<hyphen> S\<^esup>" in
                 Ring.ring_tOp_closed[of S], assumption+,
       frule mem_subring_mem_ring[of S " lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> "],
         assumption+,
       frule_tac x = "lcf R S X f" and y = "lcf R S X g\<^bsup>\<hyphen> S\<^esup>" in
         Idomain.idom_tOp_nonzeros[of S], assumption+,
       simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply(frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>" and
       y = "X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup>" in
      Idomain.idom_tOp_nonzeros[of R], assumption+,
      frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>" and
       y = "X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup>" in ring_tOp_closed,
      assumption+,
      frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
       X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup>" and y = g in
        Idomain.idom_tOp_nonzeros[of R], assumption+,
      frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
       X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup>" and y = g in ring_tOp_closed,
      assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply (frule pol_diff_deg_less[of f "s_cf R S X f"
       "s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
                 X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)"], assumption+,
       simp add:s_cf_pol_coeff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> fst (s_cf R S X f) = fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))
 2. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> snd (s_cf R S X f) (fst (s_cf R S X f)) = snd (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)))
 3. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) < fst (s_cf R S X f)\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply (simp add:s_cf_deg[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (deg_n R S X f) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (deg_n R S X g) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> deg_n R S X f = deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)
 2. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> snd (s_cf R S X f) (fst (s_cf R S X f)) = snd (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)))
 3. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) < fst (s_cf R S X f)\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply (frule deg_mult_pols[of "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> (lcf R S X g)\<^bsup>\<hyphen> S\<^esup>"
                   "(X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> )\<cdot>\<^sub>r g"], assumption+,
          rule ring_tOp_closed, assumption+,
          rule Idomain.idom_tOp_nonzeros[of R], assumption+,
          (erule conjE)+,
          subst ring_tOp_assoc[of "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>" _ g],
                 assumption+, simp,
          cut_tac pol_of_deg0[THEN sym, of "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>"],
          simp,
          thin_tac "deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
              (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)) =
               deg_n R S X (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (deg_n R S X f) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (deg_n R S X g) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>) = 0; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S\<rbrakk> \<Longrightarrow> deg_n R S X f = deg_n R S X (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)
 2. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (deg_n R S X f) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (deg_n R S X g) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) \<noteq> \<zero>; deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)) = deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>) + deg_n R S X (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)\<rbrakk> \<Longrightarrow> lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R
 3. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (deg_n R S X f) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (deg_n R S X g) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) \<noteq> \<zero>; deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)) = deg_n R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>) + deg_n R S X (X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)\<rbrakk> \<Longrightarrow> lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>
 4. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> snd (s_cf R S X f) (fst (s_cf R S X f)) = snd (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)))
 5. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) < fst (s_cf R S X f)\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply (frule deg_mult_pols[of "(X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> )" g],
          assumption+, simp,
          simp add:deg_to_X_d, assumption+,
          fold lcf_def,
          subst divisionTr0[of g "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>"
                        "fst (s_cf R S X f) - fst (s_cf R S X g)"],
          assumption+, simp add:Subring_zero_ring_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> lcf R S X f = lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g
 2. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) < fst (s_cf R S X f)\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply (subst Ring.ring_tOp_assoc, assumption+, simp add:lcf_mem,
          frule Corps.invf_inv[of S "lcf R S X g"], simp add:lcf_mem,
          simp add:Subring_zero_ring_zero, simp add:Ring.ring_r_one,
          frule s_cf_expr[of "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
               X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g"],
          rule  Idomain.idom_tOp_nonzeros[of R], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) < fst (s_cf R S X f); pol_coeff S (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) \<and> lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) \<and> snd (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) \<noteq> \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply ((erule conjE)+,
        thin_tac "snd (s_cf R S X
           (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
            X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r  g))
           (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
              X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) \<noteq> \<zero>\<^bsub>S\<^esub>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < fst (s_cf R S X g); f \<in> carrier R; f \<noteq> \<zero>; fst (s_cf R S X g) \<le> fst (s_cf R S X f); aGroup R; Idomain R; Subring R S; X \<noteq> \<zero>; X \<in> carrier R; Idomain S; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; pol_coeff S (s_cf R S X f); f = polyn_expr R X (fst (s_cf R S X f)) (s_cf R S X f); lcf R S X f \<noteq> \<zero>; pol_coeff S (s_cf R S X g); g = polyn_expr R X (fst (s_cf R S X g)) (s_cf R S X g); lcf R S X g \<noteq> \<zero>; lcf R S X f \<in> carrier S; Ring S; aGroup S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<noteq> \<zero>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)) = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) < fst (s_cf R S X f); pol_coeff S (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g)); lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = polyn_expr R X (fst (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))) (s_cf R S X (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g))\<rbrakk> \<Longrightarrow> f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (fst (s_cf R S X f) - fst (s_cf R S X g))\<^esup> \<cdot>\<^sub>r g) < fst (s_cf R S X f)
[PROOF STEP]
apply (rotate_tac -1, drule sym, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) divisionTr2:"\<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>;
                   0 < deg_n R S X g\<rbrakk>  \<Longrightarrow>  \<forall>f. div_condn R S X n g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g\<rbrakk> \<Longrightarrow> \<forall>f. div_condn R S X n g f
[PROOF STEP]
apply (cut_tac ring_is_ag,
       frule Corps.field_is_idom[of "S"],
       cut_tac subring, frule subring_Ring,
       cut_tac polyn_ring_integral, simp,
       cut_tac X_mem_R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R\<rbrakk> \<Longrightarrow> \<forall>f. div_condn R S X n g f
[PROOF STEP]
apply (rule nat_less_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f\<rbrakk> \<Longrightarrow> \<forall>f. div_condn R S X n g f
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f\<rbrakk> \<Longrightarrow> div_condn R S X n g f
[PROOF STEP]
apply (subst div_condn_def, rule impI, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (case_tac "f = \<zero>\<^bsub>R\<^esub>",
       cut_tac ring_zero,
       subgoal_tac " f \<plusminus> -\<^sub>a (\<zero> \<cdot>\<^sub>r g) = \<zero>",
       blast,
       simp add:ring_times_0_x, simp add:aGroup.ag_inv_zero[of "R"],
       simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (case_tac "n < deg_n R S X g")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; n < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
 2. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; \<not> n < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (cut_tac ring_zero,
        subgoal_tac "deg_n R S X (f \<plusminus> -\<^sub>a (\<zero> \<cdot>\<^sub>r g)) < deg_n R S X g",
        blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; n < deg_n R S X g; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> deg_n R S X (f \<plusminus> -\<^sub>a \<zero> \<cdot>\<^sub>r g) < deg_n R S X g
 2. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; \<not> n < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (
       simp add:ring_times_0_x, simp add:aGroup.ag_inv_zero,
       simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; \<not> n < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac x = n and y = "deg_n R S X g" in leI,
       thin_tac "\<not> n < deg_n R S X g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
(** deg_n R S X g \<le> deg_n R S X f **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac f = f in divisionTr1[of g], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac p = f in lcf_mem,
       frule lcf_mem[of g],
       frule lcf_nonzero[of g], assumption+,
       frule Corps.invf_closed1[of S "lcf R S X g"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S - {\<zero>\<^bsub>S\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac x = "lcf R S X f" and y = "lcf R S X g\<^bsup>\<hyphen> S\<^esup>" in
                 Ring.ring_tOp_closed[of S], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S - {\<zero>\<^bsub>S\<^esub>}; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>" in mem_subring_mem_ring,
        assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S - {\<zero>\<^bsub>S\<^esub>}; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac n = "deg_n R S X f - deg_n R S X g" in npClose[of X],
        frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup>" and
                  y = "X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup>" in
                  ring_tOp_closed, assumption+,
        frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
                       X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup>"  and
                  y = g in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S - {\<zero>\<^bsub>S\<^esub>}; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (erule disjE, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; \<forall>m<n. \<forall>f. div_condn R S X m g f; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S - {\<zero>\<^bsub>S\<^esub>}; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (drule_tac a = "deg_n R S X (f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub>
          lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g))" in
          forall_spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> n; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S - {\<zero>\<^bsub>S\<^esub>}; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; \<forall>fa. div_condn R S X (deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)) g fa\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (simp add:div_condn_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S \<and> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; \<forall>fa. fa \<in> carrier R \<and> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) = deg_n R S X fa \<longrightarrow> (\<exists>q. q \<in> carrier R \<and> (fa \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (fa \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g))\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (drule_tac x = "f \<plusminus>
             -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
                 X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r
                 g)" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S \<and> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R \<and> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) = deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) \<longrightarrow> (\<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g))\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
           X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g" in aGroup.ag_mOp_closed,
           assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S \<and> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) < deg_n R S X f; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R \<and> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) = deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) \<longrightarrow> (\<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)); -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac x = f and y = "-\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
               X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)" in
        aGroup.ag_pOp_closed, assumption+, simp,
        thin_tac "deg_n R S X (f \<plusminus>  -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
                 X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g)) < deg_n R S X f")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S \<and> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g); -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (erule exE,
        thin_tac "f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
            X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g) \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S \<and> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply ((erule conjE)+,
        frule_tac x = q and y = g in ring_tOp_closed, assumption+,
        frule_tac x = "q \<cdot>\<^sub>r g" in aGroup.ag_mOp_closed, assumption+,
        simp add:aGroup.ag_pOp_assoc,
        simp add:aGroup.ag_p_inv[THEN sym],
        simp add:ring_distrib2[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; q \<in> carrier R; f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g) < deg_n R S X g; q \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a q \<cdot>\<^sub>r g \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (frule_tac x = "lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r
         X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup>" and y = q in
                          aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; q \<in> carrier R; f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g) < deg_n R S X g; q \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a q \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a q \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q \<in> carrier R; f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g = \<zero>\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
 2. \<And>n f q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a q \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g) < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f q. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; aGroup R; Idomain R; Subring R S; Ring S; Idomain S; X \<in> carrier R; f \<in> carrier R; n = deg_n R S X f; f \<noteq> \<zero>; deg_n R S X g \<le> deg_n R S X f; lcf R S X f \<in> carrier S; lcf R S X g \<in> carrier S; lcf R S X g \<noteq> \<zero>\<^bsub>S\<^esub>; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier R; X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<cdot>\<^sub>r g \<in> carrier R; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<in> carrier S; lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<noteq> \<zero>\<^bsub>S\<^esub>; q \<in> carrier R; q \<cdot>\<^sub>r g \<in> carrier R; -\<^sub>a q \<cdot>\<^sub>r g \<in> carrier R; lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q \<in> carrier R; deg_n R S X (f \<plusminus> -\<^sub>a (lcf R S X f \<cdot>\<^sub>r\<^bsub>S\<^esub> lcf R S X g\<^bsup>\<hyphen> S\<^esup> \<cdot>\<^sub>r X^\<^bsup>R (deg_n R S X f - deg_n R S X g)\<^esup> \<plusminus> q) \<cdot>\<^sub>r g) < deg_n R S X g\<rbrakk> \<Longrightarrow> \<exists>q. q \<in> carrier R \<and> (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) divisionTr3:"\<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>;
      0 < deg_n R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow>
     \<exists>q\<in>carrier R. (f \<plusminus> -\<^sub>a (q \<cdot>\<^sub>r  g) = \<zero>) \<or> ( f \<plusminus> -\<^sub>a (q \<cdot>\<^sub>r g) \<noteq> \<zero> \<and>
      deg_n R S X (f \<plusminus> -\<^sub>a (q \<cdot>\<^sub>r g)) < (deg_n R S X g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g \<noteq> \<zero> \<and> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g
[PROOF STEP]
apply (frule divisionTr2[of g "deg_n R S X f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; \<forall>fa. div_condn R S X (deg_n R S X f) g fa\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g \<noteq> \<zero> \<and> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g
[PROOF STEP]
apply (drule_tac x = f in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Corps S; g \<in> carrier R; g \<noteq> \<zero>; 0 < deg_n R S X g; f \<in> carrier R; div_condn R S X (deg_n R S X f) g f\<rbrakk> \<Longrightarrow> \<exists>q\<in>carrier R. f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g = \<zero> \<or> f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g \<noteq> \<zero> \<and> deg_n R S X (f \<plusminus> -\<^sub>a q \<cdot>\<^sub>r g) < deg_n R S X g
[PROOF STEP]
apply (simp add:div_condn_def, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done