[STATEMENT]
lemma (in PolynRg) P_mod_diffxxx5_1:"\<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
  maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y;
  f \<in> carrier R; g \<in> carrier R; h \<in> carrier R;
  deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
             (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g);
  deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R'
                     (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f;
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
                (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g);
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
                (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h);
  rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h);
  P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h))\<rbrakk> \<Longrightarrow>
 (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m)) \<in> carrier R \<times> carrier R  \<and>
 erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))
     (fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m))) =
           erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)) \<and>
 erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t))
     (snd (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m))) =
           erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)) \<and>
     (deg R S X (fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m))) \<le> deg R'
  (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
                    (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m))))) \<and>
 P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>)) ((fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> m)) \<plusminus> -\<^sub>a
                                      (fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m)))) \<and>
 (deg R S X (snd (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m))) +
   deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
     (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m)))) \<le>  deg R S X f) \<and>
 P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc m)\<^esup>)) ((snd (Hpr\<^bsub>R S X t R' Y f g h\<^esub> m)) \<plusminus> -\<^sub>a
                                      (snd (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m)))) \<and>
 P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S (Suc (Suc m))\<^esup>)) (f \<plusminus> -\<^sub>a
  ((fst (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m))) \<cdot>\<^sub>r (snd (Hpr\<^bsub>R S X t R' Y f g h\<^esub> (Suc m)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m \<in> carrier R \<times> carrier R \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)) \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)) \<and> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc m)\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))
[PROOF STEP]
apply (frule P_mod_diffxxx5[of t R' Y f g h m], assumption+)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> (g, h) \<in> carrier R \<times> carrier R
 2. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> deg R S X (fst (g, h)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)))
 3. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> deg R S X (snd (g, h)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h))) \<le> deg R S X f
 4. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)))
 5. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)))
 6. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h))) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)))
 7. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)
 8. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m \<in> carrier R \<times> carrier R \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)) \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)) \<and> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc m)\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))\<rbrakk> \<Longrightarrow> Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m \<in> carrier R \<times> carrier R \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)) \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)) \<and> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc m\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> m) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m)) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc m)\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc m))
[PROOF STEP]
apply (simp add:cart_prod_split, simp, simp, simp, simp, simp, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in PolynRg) P_mod_diffxxx5_2:"\<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>;
  maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R;
  g \<in> carrier R; h \<in> carrier R;
  deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
               (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g);
  deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R'
                      (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f;
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
      (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g);
  0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
      (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h);
  rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g)
    (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h);
  P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a (g \<cdot>\<^sub>r h))\<rbrakk> \<Longrightarrow>
                (Hpr\<^bsub>R S X t R' Y f g h\<^esub> m) \<in> carrier R \<times> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h)\<rbrakk> \<Longrightarrow> Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R
[PROOF STEP]
apply (case_tac "m = 0", simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); 0 < m\<rbrakk> \<Longrightarrow> Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R
[PROOF STEP]
apply (frule P_mod_diffxxx5_1[of t R' Y f g h
       "m - Suc 0"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0) \<in> carrier R \<times> carrier R \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)) \<and> erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)) \<and> deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<and> deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<le> deg R S X f \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<and> P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc (m - Suc 0))\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))\<rbrakk> \<Longrightarrow> Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Idomain S; t \<in> carrier S; t \<noteq> \<zero>\<^bsub>S\<^esub>; maximal_ideal S (S \<diamondsuit>\<^sub>p t); PolynRg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y; f \<in> carrier R; g \<in> carrier R; h \<in> carrier R; deg R S X g \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); deg R S X h + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) \<le> deg R S X f; 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g); 0 < deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); rel_prime_pols R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) g) (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) h); P_mod R S X (S \<diamondsuit>\<^sub>p t) (f \<plusminus> -\<^sub>a g \<cdot>\<^sub>r h); 0 < m; Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0) \<in> carrier R \<times> carrier R; erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (g, h)); erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) = erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (snd (g, h)); deg R S X (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) \<le> deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); deg R S X (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))) + deg R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (erH R S X R' (S /\<^sub>r (S \<diamondsuit>\<^sub>p t)) Y (pj S (S \<diamondsuit>\<^sub>p t)) (fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))) \<le> deg R S X f; P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (m - Suc 0)\<^esup>)) (snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> (m - Suc 0)) \<plusminus> -\<^sub>a snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0))); P_mod R S X (S \<diamondsuit>\<^sub>p (t^\<^bsup>S Suc (Suc (m - Suc 0))\<^esup>)) (f \<plusminus> -\<^sub>a fst (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)) \<cdot>\<^sub>r snd (Hpr\<^bsub> R S X t R' Y f g h\<^esub> Suc (m - Suc 0)))\<rbrakk> \<Longrightarrow> Hpr\<^bsub> R S X t R' Y f g h\<^esub> m \<in> carrier R \<times> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done