[STATEMENT]
lemma normal_qe_pres\<^sub>1_o:
  "\<forall>a \<in> set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0 \<Longrightarrow>
   Z.normal ((qe_pres\<^sub>1 \<circ> hd_coeffs1) as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0 \<Longrightarrow> Z.normal ((qe_pres\<^sub>1 \<circ> hd_coeffs1) as)
[PROOF STEP]
supply image_cong_simp [cong del]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0 \<Longrightarrow> Z.normal ((qe_pres\<^sub>1 \<circ> hd_coeffs1) as)
[PROOF STEP]
apply(auto simp:qe_pres\<^sub>1_def Z.normal_def
   dest!:atoms_list_disjE atoms_list_conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) = []; divisor x = 0; 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as))); x \<in> set (hd_coeffs1 as); is_dvd x\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add: hd_coeffs1_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor x = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); x = Dvd (zlcms (map hd_coeff as)) 0 [1] \<or> x \<in> hd_coeff1 (zlcms (map hd_coeff as)) ` set as; is_dvd x\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor x = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd x; x = Dvd (zlcms (map hd_coeff as)) 0 [1]\<rbrakk> \<Longrightarrow> False
 2. \<And>n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor x = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd x; x \<in> hd_coeff1 (zlcms (map hd_coeff as)) ` set as\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor x = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd x; x \<in> hd_coeff1 (zlcms (map hd_coeff as)) ` set as\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac xa)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x11 x12. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Le x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac list)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x11 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Le x11 list\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac list)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n xa x11 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Le x11 list; list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x11 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Le x11 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 4. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 5. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x11 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Le x11 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac list)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 list\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac list)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 list; list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = Dvd x21 x22 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd 0 x22 (0 # lista) \<in> set as; xa = Dvd 0 x22 (0 # lista); list = 0 # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a = 0; x21 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x21 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x21 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; x21 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; x21 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:zdiv_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "a \<in> set(map hd_coeff as)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as); \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 2. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as); \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x21 x22 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as); \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis elem_le_zlcms linorder_not_le zlcms_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 list\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac list)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 list; list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); is_dvd (hd_coeff1 (zlcms (map hd_coeff as)) xa); xa \<in> set as; xa = NDvd x31 x32 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd 0 x32 (0 # lista) \<in> set as; xa = NDvd 0 x32 (0 # lista); list = 0 # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a = 0; x31 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:zdiv_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "a \<in> set(map hd_coeff as)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis elem_le_zlcms linorder_not_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); x31 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis linorder_not_le zlcms_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xa x31 x32 list a lista. \<lbrakk>0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) = []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); x31 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (hd_coeffs1 as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (hd_coeffs1 as)); x \<in> set (hd_coeffs1 as); 0 \<le> n; n < zlcms (map divisor (filter is_dvd (hd_coeffs1 as)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add: hd_coeffs1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); x = Dvd (zlcms (map hd_coeff as)) 0 [1] \<or> x \<in> hd_coeff1 (zlcms (map hd_coeff as)) ` set as; 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as))))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); x = Dvd (zlcms (map hd_coeff as)) 0 [1]\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); x \<in> hd_coeff1 (zlcms (map hd_coeff as)) ` set as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n x. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor x = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); x \<in> hd_coeff1 (zlcms (map hd_coeff as)) ` set as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac xa)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x11 x12. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Le x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac list)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x11 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Le x11 list\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac list)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b n xa x11 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Le x11 list; list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x11 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Le x11 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 4. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x11 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Le x11 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 x23. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 x23\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 list\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac list)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 list; list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = Dvd x21 x22 list; list = a # lista\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd 0 x22 (0 # lista) \<in> set as; xa = Dvd 0 x22 (0 # lista); list = 0 # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a = 0; x21 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x21 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x21 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; x21 = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; x21 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:zdiv_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "a \<in> set(map hd_coeff as)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as); \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 2. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as); \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 3. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x21 x22 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); Dvd x21 x22 (a # lista) \<in> set as; xa = Dvd x21 x22 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as); a \<in> set (map hd_coeff as); \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis elem_le_zlcms linorder_not_le zlcms_pos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 x33. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 x33\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(rename_tac list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(case_tac list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 list; list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 list; list = a # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>\<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; divisor (hd_coeff1 (zlcms (map hd_coeff as)) xa) = 0; (aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); xa \<in> set as; xa = NDvd x31 x32 list; list = a # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd 0 x32 (0 # lista) \<in> set as; xa = NDvd 0 x32 (0 # lista); list = 0 # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a = 0; x31 = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; zlcms (map hd_coeff as) div a = 0 \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:zdiv_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "a \<in> set(map hd_coeff as)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0\<rbrakk> \<Longrightarrow> a \<in> set (map hd_coeff as)
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a \<or> zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); 0 \<le> zlcms (map hd_coeff as) \<and> zlcms (map hd_coeff as) < a\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis elem_le_zlcms linorder_not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as) \<or> x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); zlcms (map hd_coeff as) \<le> 0 \<and> a < zlcms (map hd_coeff as)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis linorder_not_le zlcms_pos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b n xa x31 x32 list a lista. \<lbrakk>(aa, b) \<in> set (lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as)); 0 \<le> n; n < lcm (zlcms (map hd_coeff as)) (zlcms (map divisor (filter is_dvd (map (hd_coeff1 (zlcms (map hd_coeff as))) as)))); NDvd x31 x32 (a # lista) \<in> set as; xa = NDvd x31 x32 (a # lista); list = a # lista; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0; lbounds (Dvd (zlcms (map hd_coeff as)) 0 [1] # map (hd_coeff1 (zlcms (map hd_coeff as))) as) \<noteq> []; a \<noteq> 0; \<forall>i\<in>set (map hd_coeff as). i \<noteq> 0; a \<in> set (map hd_coeff as); x31 = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done