[STATEMENT]
lemma taq_proots_gt_code[code]:
  "TaQ_gt_rats a p q = (
    if poly p a \<noteq> 0 then
      (let
      ip = clear_de p; 
      iq = clear_de q
      in ri_changes_gt_spmods a ip (pderiv ip * iq))
    else 
       Code.abort (STR ''Roots at border yet to be supported'') 
                              (\<lambda>_. TaQ_gt_rats a p q)
    )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
proof (cases "poly p a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. poly p a = 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
 2. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
poly p a = 0

goal (2 subgoals):
 1. poly p a = 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
 2. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly p a = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly p a = 0

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
poly p a \<noteq> 0

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
define ip iq where "ip = clear_de p" and "iq = clear_de q"
[PROOF STATE]
proof (state)
this:
ip = clear_de p
iq = clear_de q

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
define dp dq where "dp = rat_of_int (de_lcm p)" and "dq = rat_of_int (de_lcm q)"
[PROOF STATE]
proof (state)
this:
dp = rat_of_int (de_lcm p)
dq = rat_of_int (de_lcm q)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
define aa where "aa = real_of_rat a"
[PROOF STATE]
proof (state)
this:
aa = real_of_rat a

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "dp > 0" "dq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < dp &&& 0 < dq
[PROOF STEP]
unfolding dp_def dq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < rat_of_int (de_lcm p) &&& 0 < rat_of_int (de_lcm q)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < dp
0 < dq

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have ip:"of_int_poly ip = smult dp p" and iq:"of_int_poly iq = smult dq q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly ip = smult dp p &&& of_int_poly iq = smult dq q
[PROOF STEP]
using clear_de
[PROOF STATE]
proof (prove)
using this:
of_int_poly (clear_de ?p) = smult (rat_of_int (de_lcm ?p)) ?p

goal (1 subgoal):
 1. of_int_poly ip = smult dp p &&& of_int_poly iq = smult dq q
[PROOF STEP]
unfolding ip_def iq_def dp_def dq_def
[PROOF STATE]
proof (prove)
using this:
of_int_poly (clear_de ?p) = smult (rat_of_int (de_lcm ?p)) ?p

goal (1 subgoal):
 1. of_int_poly (clear_de p) = smult (rat_of_int (de_lcm p)) p &&& of_int_poly (clear_de q) = smult (rat_of_int (de_lcm q)) q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_poly ip = smult dp p
of_int_poly iq = smult dq q

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0
        \<and> aa < x} 
        (map_poly real_of_rat (of_int_poly iq))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq))
[PROOF STEP]
unfolding TaQ_gt_rats_def ip iq aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. taq {x. poly (map_poly real_of_rat p) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat q) = taq {x. poly (map_poly real_of_rat (smult dp p)) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat (smult dq q))
[PROOF STEP]
using \<open>dp > 0\<close> \<open>dq >0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < dp
0 < dq

goal (1 subgoal):
 1. taq {x. poly (map_poly real_of_rat p) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat q) = taq {x. poly (map_poly real_of_rat (smult dp p)) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat (smult dq q))
[PROOF STEP]
by (simp add:of_rat_hom.map_poly_hom_smult taq_smult_pos)
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = taq {x. poly (of_int_poly ip) x = (0::real) 
        \<and> aa < x } (of_int_poly iq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq)) = taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq)
[PROOF STEP]
by (simp add:map_poly_map_poly comp_def)
[PROOF STATE]
proof (state)
this:
taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq)) = taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq)) = taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = changes_gt_smods aa (of_int_poly ip) 
      (pderiv (of_int_poly ip) * of_int_poly iq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
have "poly (map_poly of_int ip) aa \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly ip) aa \<noteq> 0
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly ip) (real_of_rat a) \<noteq> 0
[PROOF STEP]
using False \<open>0 < dp\<close> ip rat_int.map_poly_R_hom_commute
[PROOF STATE]
proof (prove)
using this:
poly p a \<noteq> 0
0 < dp
of_int_poly ip = smult dp p
poly (of_int_poly ?p) (real_of_rat ?x) = real_of_rat (poly (of_int_poly ?p) ?x)

goal (1 subgoal):
 1. poly (of_int_poly ip) (real_of_rat a) \<noteq> 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
poly (of_int_poly ip) aa \<noteq> 0

goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
from sturm_tarski_above[OF this]
[PROOF STATE]
proof (chain)
picking this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} ?q = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * ?q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} ?q = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * ?q)

goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))
[PROOF STEP]
by (simp add: of_int_hom.map_poly_pderiv of_int_poly_hom.hom_mult)
[PROOF STATE]
proof (state)
this:
changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = ri_changes_gt_spmods a ip (pderiv ip * iq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
using rat_int.changes_spmods_smods
[PROOF STATE]
proof (prove)
using this:
ri_changes_itv_spmods ?a ?b ?p ?q = changes_itv_smods (real_of_rat ?a) (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_R_spmods ?p ?q = changes_R_smods (of_int_poly ?p) (of_int_poly ?q)
ri_changes_gt_spmods ?a ?p ?q = changes_gt_smods (real_of_rat ?a) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_le_spmods ?b ?p ?q = changes_le_smods (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)

goal (1 subgoal):
 1. changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
using this:
ri_changes_itv_spmods ?a ?b ?p ?q = changes_itv_smods (real_of_rat ?a) (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_R_spmods ?p ?q = changes_R_smods (of_int_poly ?p) (of_int_poly ?q)
ri_changes_gt_spmods ?a ?p ?q = changes_gt_smods (real_of_rat ?a) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_le_spmods ?b ?p ?q = changes_le_smods (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)

goal (1 subgoal):
 1. changes_gt_smods (real_of_rat a) (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
have "TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq) "
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
unfolding Let_def ip_def iq_def
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q)

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q)
poly p a \<noteq> 0

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))

goal:
No subgoals!
[PROOF STEP]
qed