Session Virtual_Substitution

Theory QE

section "QE lemmas"
theory QE
  imports Polynomials.MPoly_Type_Univariate
    Polynomials.Polynomials  Polynomials.MPoly_Type_Class_FMap 
    "HOL-Library.Quadratic_Discriminant"
begin

(* This file may take some time to load *)

subsection "Useful Definitions/Setting Up"

definition sign:: "real Polynomial.poly  real  int"
  where "sign p x  (if poly p x = 0 then 0 else (if poly p x > 0 then 1 else -1))"

definition sign_num:: "real  int"
  where "sign_num x  (if x = 0 then 0 else (if x > 0 then 1 else -1))"

definition root_list:: "real Polynomial.poly  real set"
  where "root_list p  ({(x::real). poly p x = 0}::real set)" 

definition root_set:: "(real × real × real) set  real set"
  where "root_set les  ({(x::real). ( (a, b, c)  les. a*x^2 + b*x + c = 0)}::real set)" 

definition sorted_root_list_set:: "(real × real × real) set  real list"
  where "sorted_root_list_set p  sorted_list_of_set (root_set p)" 

definition nonzero_root_set:: "(real × real × real) set  real set"
  where "nonzero_root_set les  ({(x::real). ( (a, b, c)  les. (a  0  b  0)  a*x^2 + b*x + c = 0)}::real set)" 

definition sorted_nonzero_root_list_set:: "(real × real × real) set  real list"
  where "sorted_nonzero_root_list_set p  sorted_list_of_set (nonzero_root_set p)" 


(* Important property of sorted lists *)
lemma sorted_list_prop:
  fixes l::"real list"
  fixes x::"real"
  assumes sorted: "sorted l"
  assumes lengt: "length l > 0"
  assumes xgt: "x > l ! 0"
  assumes xlt: "x  l ! (length l - 1)"
  shows "n. (n+1) < (length l)  x  l !n  x  l ! (n + 1)"
proof - 
  have "¬(n. (n+1) < (length l)  x  l !n  x  l ! (n + 1))  False"
  proof clarsimp 
    fix n
    assume alln: "n. l ! n  x  Suc n < length l  ¬ x  l ! Suc n"
    have "k. (k < length l  x > l ! k)" 
    proof clarsimp 
      fix k
      show "k < length l  l ! k < x"
      proof (induct k)
        case 0
        then show ?case using xgt by auto
      next
        case (Suc k)
        then show ?case using alln
          using less_eq_real_def by auto 
      qed
    qed
    then show "False"
      using xlt diff_Suc_less lengt not_less
      by (metis One_nat_def) 
  qed
  then show ?thesis by auto
qed


subsection "Quadratic polynomial properties"
lemma quadratic_poly_eval: 
  fixes a b c::"real"
  fixes x::"real"
  shows "poly [:c, b, a:] x = a*x^2 + b*x + c"    
proof - 
  have "x * (b + x * a) = a * x2 + b * x" by (metis add.commute distrib_right mult.assoc mult.commute power2_eq_square)
  then show ?thesis by auto
qed

lemma poly_roots_set_same:
  fixes a b c:: "real"
  shows "{(x::real). a * x2 + b * x + c = 0} = {x. poly [:c, b, a:] x = 0}"
proof - 
  have "x. a*x^2 + b*x + c = poly [:c, b, a:] x"
  proof clarsimp 
    fix x
    show "a * x2 + b * x = x * (b + x * a)"
      using quadratic_poly_eval[of c b a x] by auto
  qed
  then show ?thesis 
    by auto
qed

lemma root_set_finite:
  assumes fin: "finite les"
  assumes nex: "¬( (a, b, c)  les. a = 0  b = 0  c = 0 )"
  shows "finite (root_set les)"
proof - 
  have "(a, b, c)  les. finite {(x::real). a*x^2 + b*x + c = 0}" 
  proof clarsimp 
    fix a b c
    assume "(a, b, c)  les"
    then have "[:c, b, a:]  0" using nex by auto
    then have "finite {x. poly [:c, b, a:] x = 0}"
      using poly_roots_finite[where p = "[:c, b, a:]"] by auto
    then show "finite {x. a * x2 + b * x + c = 0}"
      using  poly_roots_set_same by auto
  qed
  then show ?thesis using fin
    unfolding root_set_def by auto
qed

lemma nonzero_root_set_finite:
  assumes fin: "finite les"
  shows "finite (nonzero_root_set les)"
proof - 
  have "(a, b, c)  les. (a  0  b  0)  finite {(x::real). a*x^2 + b*x + c = 0}" 
  proof clarsimp 
    fix a b c
    assume ins: "(a, b, c)  les"
    assume "a = 0  b  0"
    then have "[:c, b, a:]  0" using ins by auto
    then have "finite {x. poly [:c, b, a:] x = 0}"
      using poly_roots_finite[where p = "[:c, b, a:]"] by auto
    then show "finite {x. a * x2 + b * x + c = 0}"
      using  poly_roots_set_same by auto
  qed
  then show ?thesis using fin
    unfolding nonzero_root_set_def by auto
qed

lemma discriminant_lemma:
  fixes a b c r::"real"
  assumes aneq: "a  0"
  assumes beq: "b = 2 * a * r"
  assumes root: " a * r^2 - 2 * a * r*r + c = 0"
  shows "x. a * x2 + b * x + c = 0  x = -r"
proof - 
  have "c = a*r^2" using root
    by (simp add: power2_eq_square)
  then have same: "b^2 - 4*a*c = (2 * a * r)^2 - 4*a*(a*r^2)" using beq
    by blast 
  have "(2 * a * r)^2 = 4*a^2*r^2"
    by (simp add: mult.commute power2_eq_square)
  then have "(2 * a * r)^2 - 4*a*(a*(r)^2) = 0"
    using power2_eq_square by auto 
  then have "b^2 - 4*a*c = 0" using same
    by simp 
  then have "x. a * x2 + b * x + c = 0  x = -b / (2 * a)"
    using discriminant_zero aneq unfolding discrim_def by auto
  then show ?thesis using beq
    by (simp add: aneq) 
qed

(* Show a polynomial only changes sign when it passes through a root *)
lemma changes_sign:
  fixes p:: "real Polynomial.poly"
  shows "x::real.  y::real. ((sign p x  sign p y   x < y)  (c  (root_list p). x  c  c  y))"
proof clarsimp
  fix x y
  assume "sign p x  sign p y"
  assume "x < y"
  then show "croot_list p. x  c  c  y"
    using poly_IVT_pos[of x y p] poly_IVT_neg[of x y p] 
    by (metis (mono_tags) ‹sign p x  sign p y less_eq_real_def linorder_neqE_linordered_idom mem_Collect_eq root_list_def sign_def)
qed

(* Show a polynomial only changes sign if it passes through a root *)
lemma changes_sign_var:
  fixes a b c x y:: "real"
  shows "((sign_num (a*x^2 + b*x + c)  sign_num (a*y^2 + b*y + c)   x < y)  (q. (a*q^2 + b*q + c = 0  x  q  q  y)))"
proof  clarsimp
  assume sn: "sign_num (a * x2 + b * x + c)  sign_num (a * y2 + b * y + c)"
  assume xy: " x < y"
  let ?p = "[:c, b, a:]"
  have cs: "((sign ?p x  sign ?p y   x < y)  (c  (root_list ?p). x  c  c  y))"
    using changes_sign[of ?p] by auto
  have "(sign ?p x  sign ?p y   x < y)"
    using sn xy unfolding sign_def sign_num_def using quadratic_poly_eval
    by presburger 
  then have "(c  (root_list ?p). x  c  c  y)" 
    using cs 
    by auto 
  then obtain q where "q  root_list ?p  x  q  q  y" 
    by auto
  then have "a*q^2 + b*q + c = 0  x  q  q  y"
    unfolding root_list_def using quadratic_poly_eval[of c b a q]
    by auto
  then show "q. a * q2 + b * q + c = 0  x  q  q  y"  
    by auto
qed

subsection "Continuity Properties"
lemma continuity_lem_eq0:
  fixes p::"real"
  shows "r < p  x{r <..p}. a * x2 + b * x + c = 0  (a = 0  b = 0  c = 0)" 
proof - 
  assume r_lt: "r < p"
  assume inf_zer: "x{r <..p}. a * x2 + b * x + c = 0"
  have nf: "¬finite {r..<p}" using Set_Interval.dense_linorder_class.infinite_Ioo r_lt by auto
  have "¬(a = 0  b = 0  c = 0)  False"
  proof - 
    assume "¬(a = 0  b = 0  c = 0)"
    then have "[:c, b, a:]  0" by auto
    then have fin: "finite {x. poly [:c, b, a:] x = 0}" using poly_roots_finite[where p = "[:c, b, a:]"] by auto
    have "{x. a*x^2 + b*x + c = 0} = {x. poly [:c, b, a:] x = 0}" using quadratic_poly_eval by auto
    then have finset: "finite {x. a*x^2 + b*x + c = 0}"  using fin by auto
    have "{r <..p}  {x. a*x^2 + b*x + c = 0}" using inf_zer by blast
    then show "False" using finset nf
      using finite_subset
      by (metis (no_types, lifting) infinite_Ioc_iff r_lt) 
  qed
  then show "(a = 0  b = 0  c = 0)" by auto
qed

lemma continuity_lem_lt0: 
  fixes r:: "real"
  fixes a b c:: "real"
  shows "poly [:c, b, a:] r < 0 
    y'> r. x{r<..y'}. poly [:c, b, a:] x < 0"
proof - 
  let ?f = "poly [:c,b,a:]"
  assume r_ltz: "poly [:c, b, a:] r < 0"
  then have "[:c, b, a:]  0" by auto
  then have "finite {x. poly [:c, b, a:] x = 0}" using poly_roots_finite[where p = "[:c, b, a:]"]    
    by auto
  then have fin: "finite  {x. x > r  poly [:c, b, a:] x = 0}"
    using finite_Collect_conjI by blast 
  let ?l = "sorted_list_of_set {x. x > r  poly [:c, b, a:] x = 0}"
  show ?thesis proof (cases "length ?l = 0")
    case True
    then have no_zer: "¬(x>r. poly [:c, b, a:] x = 0)" using sorted_list_of_set_eq_Nil_iff fin by auto
    then have "y. y > r  y < (r + 1)  poly [:c, b, a:] y < 0 " 
    proof - 
      fix y
      assume "y > r  y < r + 1"
      then show "poly [:c, b, a:] y < 0"
        using r_ltz no_zer poly_IVT_pos[where a = "r", where p = "[:c, b, a:]", where b = "y"]
        by (meson linorder_neqE_linordered_idom)
    qed
    then show ?thesis
      by (metis (no_types, hide_lams) ¬ (x>r. poly [:c, b, a:] x = 0) ‹poly [:c, b, a:] r < 0 greaterThanAtMost_iff linorder_neqE_linordered_idom linordered_field_no_ub poly_IVT_pos) 
  next
    case False
    then have len_nonz: "length (sorted_list_of_set {x. r < x  poly [:c, b, a:] x = 0})  0"
      by blast 
    then have "n  {x. x > r  poly [:c, b, a:] x = 0}. (nth_default 0 ?l 0)  n"
      using fin set_sorted_list_of_set sorted_sorted_list_of_set
      using  in_set_conv_nth leI not_less0 sorted_nth_mono
      by (smt not_less_iff_gr_or_eq nth_default_def)
    then have no_zer: "¬(x>r. (x < (nth_default 0 ?l 0)  poly [:c, b, a:] x = 0))"
      using sorted_sorted_list_of_set by auto
    then have fa: "y. y > r  y < (nth_default 0 ?l 0)  poly [:c, b, a:] y < 0 " 
    proof - 
      fix y
      assume "y > r  y < (nth_default 0 ?l 0)"
      then show "poly [:c, b, a:] y < 0"
        using r_ltz no_zer poly_IVT_pos[where a = "r", where p = "[:c, b, a:]", where b = "y"]
        by (meson less_imp_le less_le_trans linorder_neqE_linordered_idom)
    qed
    have "nth_default 0 ?l 0 > r" using fin set_sorted_list_of_set
      using len_nonz length_0_conv length_greater_0_conv mem_Collect_eq nth_mem
      by (metis (no_types, lifting) nth_default_def)
    then have "(y'::real). r < y'  y' < (nth_default 0 ?l 0)"
      using dense by blast
    then obtain y' where y_prop:"r < y' y' < (nth_default 0 ?l 0)" by auto
    then have "x{r<..y'}. poly [:c, b, a:] x < 0"
      using fa by auto
    then show ?thesis using y_prop by blast 
  qed
qed

lemma continuity_lem_gt0: 
  fixes r:: "real"
  fixes a b c:: "real"
  shows "poly [:c, b, a:] r > 0 
    y'> r. x{r<..y'}. poly [:c, b, a:] x > 0"
proof -
  assume r_gtz: "poly [:c, b, a:] r > 0 "
  let ?p = "[:-c, -b, -a:]"
  have revpoly: "x. -1*(poly [:c, b, a:] x) = poly [:-c, -b, -a:] x"
    by (metis (no_types, hide_lams) Polynomial.poly_minus add.inverse_neutral minus_pCons mult_minus1)
  then have "poly ?p r < 0" using r_gtz
    by (metis mult_minus1 neg_less_0_iff_less)
  then have "y'> r. x{r<..y'}. poly ?p x < 0" using continuity_lem_lt0
    by blast
  then obtain y' where y_prop: "y' > r  (x{r<..y'}. poly ?p x < 0)" by auto
  then have "x{r<..y'}. poly [:c, b, a:] x > 0 " using revpoly
    using neg_less_0_iff_less by fastforce
  then show ?thesis 
    using y_prop  by blast 
qed

lemma continuity_lem_lt0_expanded: 
  fixes r:: "real"
  fixes a b c:: "real"
  shows "a*r^2 + b*r + c < 0 
    y'> r. x{r<..y'}. a*x^2 + b*x + c < 0"
  using quadratic_poly_eval continuity_lem_lt0 
  by (simp add: add.commute) 

lemma continuity_lem_gt0_expanded: 
  fixes r:: "real"
  fixes a b c:: "real"
  fixes k::"real"
  assumes kgt: "k > r"
  shows "a*r^2 + b*r + c > 0 
    x{r<..k}. a*x^2 + b*x + c > 0"
proof -
  assume "a*r^2 + b*r + c > 0"
  then have "y'> r. x{r<..y'}. poly [:c, b, a:] x > 0"
    using continuity_lem_gt0 quadratic_poly_eval[of c b a r] by auto 
  then obtain y' where y_prop: "y' > r  (x{r<..y'}. poly [:c, b, a:] x > 0)" by auto
  then have "q. q > r  q < min k y'" using kgt dense
    by (metis min_less_iff_conj)   
  then obtain q where q_prop: "q > r q < min k y'" by auto
  then have "a*q^2 + b*q + c > 0" using y_prop  quadratic_poly_eval[of c b a q]
    by (metis greaterThanAtMost_iff less_eq_real_def min_less_iff_conj)
  then show ?thesis
    using q_prop by auto
qed

subsection "Negative Infinity (Limit) Properties"

lemma ysq_dom_y: 
  fixes b:: "real"
  fixes c:: "real"
  shows "(w::real). (y:: real). (y < w  y^2 > b*y)"
proof - 
  have c1: "b  0 ==> (w::real). (y:: real). (y < w  y^2 > b*y)"
  proof - 
    assume "b  0"
    then have p1: "(y:: real). (y < -1  y*b  0)"
      by (simp add: mult_nonneg_nonpos2)
    have p2: "(y:: real). (y < -1  y^2 > 0)"
      by auto 
    then have h1: "(y:: real). (y < -1  y^2 > b*y)"  
      using p1 p2
      by (metis less_eq_real_def less_le_trans mult.commute) 
    then show ?thesis by auto
  qed
  have c2: "b < 0  b > -1 ==> (w::real). (y:: real). (y < w  y^2 > b*y)"
  proof - 
    assume "b < 0  b > -1 "
    then have h1: "(y:: real). (y < -1  y^2 > b*y)"
      by (simp add: power2_eq_square)  
    then show ?thesis by auto
  qed   
  have c3: "b  -1 ==> (w::real). (y:: real). (y < w  y^2 > b*y)"
  proof - 
    assume "b  -1 "
    then have h1: "(y:: real). (y < b  y^2 > b*y)"
      by (metis le_minus_one_simps(3) less_irrefl less_le_trans mult.commute mult_less_cancel_left power2_eq_square)
    then show ?thesis by auto
  qed   
  then  show ?thesis using c1 c2 c3
    by (metis less_trans linorder_not_less) 
qed

lemma ysq_dom_y_plus_coeff: 
  fixes b:: "real"
  fixes c:: "real"
  shows "(w::real). (y::real). (y < w  y^2 > b*y + c)"
proof - 
  have "(w::real). (y:: real). (y < w  y^2 > b*y)" using ysq_dom_y by auto
  then obtain w where w_prop: "(y:: real). (y < w  y^2 > b*y)" by auto
  have "c  0   (y::real). (y < w  y^2 > b*y + c)"
    using w_prop by auto 
  then have c1: "c  0  (w::real). (y::real). (y < w  y^2 > b*y + c)" by auto
  have "(w::real). (y:: real). (y < w  y^2 > (b-c)*y)" using ysq_dom_y by auto
  then obtain k where k_prop: "(y:: real). (y < k  y^2 > (b-c)*y)" by auto
  let ?mn = "min k (-1)"
  have "(c> 0  ( y < -1. -c*y > c))" 
  proof - 
    assume cgt: " c> 0"
    show "(y::real) < -1. -c*y > c"
    proof clarsimp
      fix y::"real"
      assume "y < -1"
      then have "-y > 1"
        by auto
      then have "c < c*(-y)" using cgt 
        by (metis 1 < - y mult.right_neutral mult_less_cancel_left_pos)
      then show " c < - (c * y) "
        by auto
    qed
  qed
  then have "(c> 0  ( y < ?mn. (b-c)*y > b*y + c))" 
    by (simp add: left_diff_distrib) 
  then have c2:  "c > 0   (y::real). (y < ?mn  y^2 > b*y + c)"
    using k_prop
    by force
  then have c2:  "c > 0  (w::real). (y::real). (y < w  y^2 > b*y + c)"
    by blast
  show ?thesis using c1 c2
    by fastforce
qed

lemma ysq_dom_y_plus_coeff_2: 
  fixes b:: "real"
  fixes c:: "real"
  shows "(w::real). (y::real). (y > w  y^2 > b*y + c)"
proof - 
  have "(w::real). (y::real). (y < w  y^2 > -b*y + c)"
    using ysq_dom_y_plus_coeff[where b = "-b", where c = "c"] by auto
  then obtain w where w_prop: "(y::real). (y < w  y^2 > -b*y + c)" by auto
  let ?mn = "min w (-1)"
  have "(y::real). (y < ?mn  y^2 > -b*y + c)" using w_prop by auto
  then have "(y::real). (y > (-1*?mn)  y^2 > b*y + c)"
    by (metis (no_types, hide_lams) add.inverse_inverse minus_less_iff mult_minus1 mult_minus_left mult_minus_right power2_eq_square) 
  then show ?thesis by auto
qed

lemma neg_lc_dom_quad: 
  fixes a:: "real"
  fixes b:: "real"
  fixes c:: "real"
  assumes alt: "a < 0"
  shows "(w::real). (y::real). (y > w  a*y^2 + b*y + c < 0)"
proof -
  have "(w::real). (y::real). (y > w  y^2 > (-b/a)*y + (-c/a))"
    using ysq_dom_y_plus_coeff_2[where b = "-b/a", where c = "-c/a"] by auto
  then have keyh: "(w::real). (y::real). (y > w  a*y^2 < a*((-b/a)*y + (-c/a)))"
    using alt by auto
  have simp1: "y. a*((-b/a)*y + (-c/a)) = a*(-b/a)*y + a*(-c/a)"
    using diff_divide_eq_iff by fastforce
  have simp2: "y. a*(-b/a)*y + a*(-c/a) = -b*y + a*(-c/a)"
    using assms by auto
  have simp3: "y. -b*y + a*(-c/a) = -b*y - c"
    using assms by auto
  then have "y. a*((-b/a)*y + (-c/a)) = -b*y - c" using simp1 simp2 simp3 by auto
  then have keyh2: "(w::real). (y::real). (y > w  a*y^2 < -b*y-c)"
    using keyh by auto
  have "y. a*y^2 < -b*y-c  a*y^2 + b*y + c < 0" by auto
  then show ?thesis using keyh2 by auto
qed

lemma pos_lc_dom_quad: 
  fixes a:: "real"
  fixes b:: "real"
  fixes c:: "real"
  assumes alt: "a > 0"
  shows "(w::real). (y::real). (y > w  a*y^2 + b*y + c > 0)"
proof -
  have "-a < 0" using alt
    by simp 
  then have "(w::real). (y::real). (y > w  -a*y^2 - b*y - c < 0)"
    using neg_lc_dom_quad[where a = "-a", where b = "-b", where c = "-c"] by auto
  then obtain w where w_prop: "(y::real). (y > w  -a*y^2 - b*y - c < 0)" by auto
  then have "(y::real). (y > w  a*y^2 + b*y + c > 0)"
    by auto
  then show ?thesis by auto
qed

(* lemma interval_infinite: 
  fixes r p::"real"
  assumes "r < p"
  shows "infinite {r<..<p}"
  using Set_Interval.dense_linorder_class.infinite_Ioo using assms by blast 
*)

subsection "Infinitesimal and Continuity Properties"
lemma les_qe_inf_helper: 
  fixes q:: "real"
  shows"((d, e, f)set les. y'> q. x{q<..y'}. d * x2 + e * x + f < 0)  
    (y'>q. ((d, e, f)set les. x{q<..y'}. d * x2 + e * x + f < 0))"
proof (induct les)
  case Nil
  then show ?case using gt_ex by auto 
next
  case (Cons z les)
  have "aset les. case a of (d, e, f)  y'>q. x{q<..y'}. d * x2 + e * x + f < 0"
    using  Cons.prems by auto
  then have " y'>q. aset les. case a of (d, e, f)  x{q<..y'}. d * x2 + e * x + f < 0"
    using Cons.hyps by auto
  then obtain y1 where y1_prop : "y1>q  (aset les. case a of (d, e, f)  x{q<..y1}. d * x2 + e * x + f < 0)"
    by auto
  have "case z of (d, e, f)  y'>q. x{q<..y'}. d * x2 + e * x + f < 0"
    using Cons.prems by auto
  then obtain y2 where y2_prop: "y2>q  (case z of (d, e, f)  (x{q<..y2}. d * x2 + e * x + f < 0))"
    by auto
  let ?y = "min y1 y2"
  have "?y > q  (aset (z#les). case a of (d, e, f)  x{q<..?y}. d * x2 + e * x + f < 0)"
    using y1_prop y2_prop
    by force
  then show ?case
    by blast
qed 

lemma have_inbetween_point_les:
  fixes r::"real"
  assumes "((d, e, f)set les. y'>r. x{r<..y'}. d * x2 + e * x + f < 0)"
  shows "(x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
proof -
  have "((d, e, f)set les. y'>r. x{r<..y'}. d * x2 + e * x + f < 0)  
    (y'>r. ((d, e, f)set les. x{r<..y'}. d * x2 + e * x + f < 0))"
    using les_qe_inf_helper assms by auto
  then have "(y'>r. ((d, e, f)set les. x{r<..y'}. d * x2 + e * x + f < 0))"
    using assms
    by blast 
  then obtain y where y_prop: "y > r   ((d, e, f)set les. x{r<..y}. d * x2 + e * x + f < 0)"
    by auto
  have "q. q >  r q < y" using y_prop dense by auto
  then obtain q where q_prop: "q > r  q < y" by auto
  then have "((d, e, f)set les. d*q^2 + e*q + f < 0)"
    using y_prop by auto
  then show ?thesis
    by auto
qed

lemma one_root_a_gt0: 
  fixes a b c r:: "real"
  shows "y'. b = 2 * a * r 
          ¬ a < 0 
          a * r^2 - 2 * a *r*r + c = 0 
          - r < y' 
          x{-r<..y'}. ¬ a * x2 + 2 * a * r*x + c < 0"
proof - 
  fix y'
  assume beq: "b = 2 * a * r"
  assume aprop: " ¬ a < 0"
  assume root: " a * r2 - 2 * a *r*r + c = 0"
  assume rootlt: "- r < y'"
  show " x{- r<..y'}. ¬ a * x2 + 2 * a* r*x+ c < 0"
  proof - 
    have h: "a = 0  (b = 0  c = 0)" using beq root   
      by auto
    then have aeq: "a = 0  x{- r<..y'}. ¬ a * x2 + 2 * a*r*x + c < 0"
      using rootlt
      by (metis add.left_neutral continuity_lem_eq0 less_numeral_extra(3) mult_zero_left mult_zero_right) 
    then have alt: "a > 0  x{- r<..y'}. ¬ a * x2 + 2 * a *r*x + c < 0"
    proof - 
      assume agt: "a > 0"
      then have "(w::real). (y::real). (y > w  a*y^2 + b*y + c > 0)"
        using pos_lc_dom_quad by auto
      then obtain w where w_prop: "y::real. (y > w  a*y^2 + b*y + c > 0)" by auto
      have isroot: "a*(-r)^2 + b*(-r) + c = 0" using root beq by auto
      then have wgteq: "w  -(r)"
      proof -
        have "w < -r  False"
          using w_prop isroot by auto
        then show ?thesis
          using not_less by blast 
      qed
      then have w1: "w + 1 > -r"
        by auto 
      have w2: "a*(w + 1)^2 + b*(w+1) + c > 0" using w_prop by auto
      have rootiff: "x. a * x2 + b * x + c = 0  x = -r" using  discriminant_lemma[where a = "a", where b = "b", where c= "c", where r = "r"]
          isroot agt beq by auto
      have allgt: "x > -r. a*x^2 + b*x + c > 0"
      proof clarsimp 
        fix x
        assume "x > -r"
        have xgtw:  "x > w + 1  a*x^2 + b*x + c > 0 "
          using w1 w2 rootiff  poly_IVT_neg[where a = "w+1", where b = "x", where p = "[:c,b,a:]"] 
            quadratic_poly_eval
          by (metis less_eq_real_def linorder_not_less) 
        have xltw: "x < w + 1  a*x^2 + b*x + c > 0"
          using w1 w2 rootiff poly_IVT_pos[where a= "x", where b = "w + 1", where p = "[:c,b,a:]"]
            quadratic_poly_eval less_eq_real_def linorder_not_less
          by (metis - r < x)
        then show "a*x^2 + b*x + c > 0"
          using w2 xgtw xltw by fastforce 
      qed
      have "z. z > -r  z < y'" using rootlt dense[where x = "-r", where y = "y'"] 
        by auto
      then obtain z where z_prop: " z > -r  z  < y'" by auto
      then have "a*z^2 + b*z + c > 0" using allgt by auto
      then show ?thesis using z_prop
        using beq greaterThanAtMost_iff by force 
    qed
    then show ?thesis using aeq alt aprop
      by linarith
  qed
qed

lemma leq_qe_inf_helper: 
  fixes q:: "real"
  shows"((d, e, f)set leq. y'> q. x{q<..y'}. d * x2 + e * x + f  0)  
    (y'>q. ((d, e, f)set leq. x{q<..y'}. d * x2 + e * x + f  0))"
proof (induct leq)
  case Nil
  then show ?case using gt_ex by auto 
next
  case (Cons z leq)
  have "aset leq. case a of (d, e, f)  y'>q. x{q<..y'}. d * x2 + e * x + f  0"
    using  Cons.prems by auto
  then have " y'>q. aset leq. case a of (d, e, f)  x{q<..y'}. d * x2 + e * x + f  0"
    using Cons.hyps by auto
  then obtain y1 where y1_prop : "y1>q  (aset leq. case a of (d, e, f)  x{q<..y1}. d * x2 + e * x + f  0)"
    by auto
  have "case z of (d, e, f)  y'>q. x{q<..y'}. d * x2 + e * x + f  0"
    using Cons.prems by auto
  then obtain y2 where y2_prop: "y2>q  (case z of (d, e, f)  (x{q<..y2}. d * x2 + e * x + f  0))"
    by auto
  let ?y = "min y1 y2"
  have "?y > q  (aset (z#leq). case a of (d, e, f)  x{q<..?y}. d * x2 + e * x + f  0)"
    using y1_prop y2_prop
    by force
  then show ?case
    by blast
qed 

lemma neq_qe_inf_helper: 
  fixes q:: "real"
  shows"((d, e, f)set neq. y'> q. x{q<..y'}. d * x2 + e * x + f  0)  
    (y'>q. ((d, e, f)set neq. x{q<..y'}. d * x2 + e * x + f  0))"
proof (induct neq)
  case Nil
  then show ?case using gt_ex by auto 
next
  case (Cons z neq)
  have "aset neq. case a of (d, e, f)  y'>q. x{q<..y'}. d * x2 + e * x + f  0"
    using  Cons.prems by auto
  then have " y'>q. aset neq. case a of (d, e, f)  x{q<..y'}. d * x2 + e * x + f  0"
    using Cons.hyps by auto
  then obtain y1 where y1_prop : "y1>q  (aset neq. case a of (d, e, f)  x{q<..y1}. d * x2 + e * x + f  0)"
    by auto
  have "case z of (d, e, f)  y'>q. x{q<..y'}. d * x2 + e * x + f  0"
    using Cons.prems by auto
  then obtain y2 where y2_prop: "y2>q  (case z of (d, e, f)  (x{q<..y2}. d * x2 + e * x + f  0))"
    by auto
  let ?y = "min y1 y2"
  have "?y > q  (aset (z#neq). case a of (d, e, f)  x{q<..?y}. d * x2 + e * x + f  0)"
    using y1_prop y2_prop
    by force
  then show ?case
    by blast
qed 


subsection "Some Casework"

lemma quadratic_shape1a:
  fixes a b c x y::"real"
  assumes agt: "a > 0"
  assumes xyroots: "x < y  a*x^2 + b*x + c = 0  a*y^2 + b*y + c = 0"
  shows "z. (z > x  z < y  a*z^2 + b*z + c < 0)"
proof clarsimp 
  fix z
  assume zgt: "z > x"
  assume zlt: "z < y"
  have frac_gtz: "(1/(2*a)) > 0" using agt
    by simp 
  have xy_prop:"(x = (-b + sqrt(b^2 - 4*a*c))/(2*a)  y = (-b - sqrt(b^2 - 4*a*c))/(2*a))
     (y = (-b + sqrt(b^2 - 4*a*c))/(2*a)  x = (-b - sqrt(b^2 - 4*a*c))/(2*a))" 
    using xyroots agt discriminant_iff unfolding discrim_def by auto   
  have "b^2 - 4*a*c  0" using xyroots discriminant_iff
    using assms(1) discrim_def by auto 
  then have pos_discrim: "b^2 - 4*a*c > 0" using xyroots discriminant_zero
    using 0  b2 - 4 * a * c assms(1) discrim_def less_eq_real_def linorder_not_less
    by metis
  then have sqrt_gt: "sqrt(b^2 - 4*a*c) > 0"
    using real_sqrt_gt_0_iff by blast 
  then have "(- b - sqrt(b^2 - 4*a*c)) < (- b + sqrt(b^2 - 4*a*c))"
    by auto
  then have "(- b - sqrt(b^2 - 4*a*c))*(1/(2*a)) < (- b + sqrt(b^2 - 4*a*c))*(1/(2*a)) "
    using frac_gtz
    by (simp add: divide_strict_right_mono) 
  then have "(- b - sqrt(b^2 - 4*a*c))/(2*a) < (- b + sqrt(b^2 - 4*a*c))/(2*a)"
    by auto
  then have xandy: "x = (- b - sqrt(b^2 - 4*a*c))/(2*a)  y = (- b + sqrt(b^2 - 4*a*c))/(2*a)"
    using xy_prop xyroots by auto
  let ?mdpt = "-b/(2*a)"
  have xlt: "x < ?mdpt"
    using xandy sqrt_gt using frac_gtz divide_minus_left divide_strict_right_mono sqrt_gt
    by (smt (verit) agt)
  have ylt: "?mdpt < y"
    using xandy sqrt_gt frac_gtz
    by (smt (verit, del_insts) divide_strict_right_mono zero_less_divide_1_iff) 
  have mdpt_val: "a*?mdpt^2 + b*?mdpt + c < 0"
  proof - 
    have firsteq: "a*?mdpt^2 + b*?mdpt + c = (a*b^2)/(4*a^2) - (b^2)/(2*a) + c"
      by (simp add: power2_eq_square) 
    have h1: "(a*b^2)/(4*a^2) = (b^2)/(4*a)"
      by (simp add: power2_eq_square)
    have h2: "(b^2)/(2*a) = (2*b^2)/(4*a)"
      by linarith
    have h3: "c = (4*a*c)/(4*a)"
      using agt by auto 
    have "a*?mdpt^2 + b*?mdpt + c = (b^2)/(4*a) - (2*b^2)/(4*a) + (4*a*c)/(4*a) "
      using firsteq h1 h2 h3
      by linarith 
    then have "a*?mdpt^2 + b*?mdpt + c = (b^2 - 2*b^2 + 4*a*c)/(4*a)"
      by (simp add: diff_divide_distrib)
    then have eq2: "a*?mdpt^2 + b*?mdpt + c = (4*a*c - b^2)/(4*a)"
      by simp
    have h: "4*a*c - b^2 < 0" using pos_discrim by auto
    have "1/(4*a) > 0" using agt by auto
    then have "(4*a*c - b^2)*(1/(4*a)) < 0"
      using h
      using mult_less_0_iff by blast 
    then show ?thesis using eq2 by auto
  qed
  have nex: "¬ (k> x. k < y  poly [:c, b, a:] k = 0)"
    using discriminant_iff agt
    by (metis (no_types, hide_lams) discrim_def order_less_irrefl quadratic_poly_eval xandy) 
  have nor2: "¬ (x>z. x < - b / (2 * a)  poly [:c, b, a:] x = 0)"
    using nex xlt ylt zgt zlt by auto
  have nor: "¬ (x>- b / (2 * a). x < z  poly [:c, b, a:] x = 0)"
    using nex xlt ylt zgt zlt discriminant_iff agt  by auto 
  then have mdpt_lt: "?mdpt < z  a*z^2 + b*z + c < 0 "
    using mdpt_val zgt zlt xlt ylt poly_IVT_pos[where p = "[:c, b, a:]", where a= "?mdpt", where b = "z"] 
      quadratic_poly_eval[of c b a]
    by (metis ¬ (k>x. k < y  poly [:c, b, a:] k = 0) linorder_neqE_linordered_idom) 
  have mdpt_gt: "?mdpt > z  a*z^2 + b*z + c < 0 "
    using zgt zlt mdpt_val xlt ylt nor2 poly_IVT_neg[where p = "[:c, b, a:]", where a = "z", where b = "?mdpt"] quadratic_poly_eval[of c b a]
    by (metis linorder_neqE_linordered_idom nex) 
  then show "a*z^2 + b*z + c < 0" 
    using mdpt_lt mdpt_gt mdpt_val by fastforce 
qed

lemma quadratic_shape1b:
  fixes a b c x y::"real"
  assumes agt: "a > 0"
  assumes xy_roots: "x < y  a*x^2 + b*x + c = 0  a*y^2 + b*y + c = 0"
  shows "z. (z > y  a*z^2 + b*z + c > 0)"
proof - 
  fix z
  assume z_gt :"z > y"
  have nogt: "¬(w. w > y  a*w^2 + b*w + c = 0)" using xy_roots discriminant_iff
    by (metis agt less_eq_real_def linorder_not_less)
  have "(w::real). (y::real). (y > w  a*y^2 + b*y + c > 0)"
    using agt pos_lc_dom_quad by auto
  then have "k > y.  a*k^2 + b*k + c > 0"
    by (metis add.commute agt less_add_same_cancel1 linorder_neqE_linordered_idom pos_add_strict) 
  then obtain k where k_prop: "k > y  a*k^2 + b*k + c > 0" by auto
  have kgt: "k > z  a*z^2 + b*z + c > 0" 
  proof - 
    assume kgt: "k > z"
    then have zneq: "a*z^2 + b*z + c = 0  False"
      using nogt  using z_gt by blast 
    have znlt: "a*z^2 + b*z + c < 0  False"
      using kgt k_prop quadratic_poly_eval[of c b a] z_gt  nogt poly_IVT_pos[where a= "z", where b = "k", where p = "[:c, b, a:]"]
      by (metis less_eq_real_def less_le_trans)
    then show "a*z^2 + b*z + c > 0" using zneq znlt
      using linorder_neqE_linordered_idom by blast 
  qed
  have klt: "k < z  a*z^2 + b*z + c > 0" 
  proof - 
    assume klt: "k < z"
    then have zneq: "a*z^2 + b*z + c = 0  False"
      using nogt using z_gt by blast 
    have znlt: "a*z^2 + b*z + c < 0  False"
      using klt k_prop quadratic_poly_eval[of c b a] z_gt  nogt poly_IVT_neg[where a= "k", where b = "z", where p = "[:c, b, a:]"]
      by (metis add.commute add_less_cancel_left add_mono_thms_linordered_field(3) less_eq_real_def)
    then show "a*z^2 + b*z + c > 0" using zneq znlt
      using linorder_neqE_linordered_idom by blast 
  qed
  then show "a*z^2 + b*z + c > 0" using k_prop kgt klt
    by fastforce 
qed

lemma quadratic_shape2a:
  fixes a b c x y::"real"
  assumes "a < 0"
  assumes "x < y  a*x^2 + b*x + c = 0  a*y^2 + b*y + c = 0"
  shows "z. (z > x  z < y  a*z^2 + b*z + c > 0)"
  using quadratic_shape1a[where a= "-a", where b = "-b", where c = "-c", where x = "x", where y = "y"]
  using assms(1) assms(2) by fastforce 

lemma quadratic_shape2b:
  fixes a b c x y::"real"
  assumes "a < 0"
  assumes "x < y  a*x^2 + b*x + c = 0  a*y^2 + b*y + c = 0"
  shows "z. (z > y  a*z^2 + b*z + c < 0)"
  using quadratic_shape1b[where a= "-a", where b = "-b", where c = "-c", where x = "x", where y = "y"]
  using assms(1) assms(2) by force 

lemma case_d1:
  fixes a b c r::"real"
  shows "b < 2 * a * r 
    a * r^2 - b*r + c = 0 
    y'>- r. x{-r<..y'}. a * x2 + b * x + c < 0"
proof - 
  assume b_lt: "b < 2*a*r"
  assume root: "a*r^2 - b*r + c = 0"
  then have "c = b*r - a*r^2" by auto
  have aeq: "a = 0  y'>- r. x{-r<..y'}. a * x2 + b * x + c < 0"
  proof - 
    assume azer: "a = 0"
    then have bltz: "b < 0" using b_lt by auto
    then have "c = b*r" using azer root by auto
    then have eval: "x. a*x^2 + b*x + c = b*(x + r)" using azer
      by (simp add: distrib_left) 
    have "x > -r. b*(x + r) < 0" 
    proof clarsimp 
      fix x
      assume xgt: "- r < x"
      then have "x + r > 0"
        by linarith 
      then show "b * (x + r) < 0"
        using bltz using mult_less_0_iff by blast 
    qed
    then show ?thesis using eval
      using less_add_same_cancel1 zero_less_one
      by (metis greaterThanAtMost_iff)
  qed
  have aneq: "a  0 y'>- r. x{-r<..y'}. a * x2 + b * x + c < 0"
  proof - 
    assume aneq: "(a::real)  0"
    have "b^2 - 4*a*c < 0  a * r2 + b * r + c  0" using root discriminant_negative[of a b c r] unfolding discrim_def 
      using aneq by auto
    then have " a * r2 + b * r + c  0 
    a * r2 - b * r + c = 0 
    b2 < 4 * a * c  False"
    proof -
      assume a1: "a * r2 - b * r + c = 0"
      assume a2: "b2 < 4 * a * c"
      have f3: "(0  - 1 * (4 * a * c) + (- 1 * b)2) = (4 * a * c + - 1 * (- 1 * b)2  0)"
        by simp
      have f4: "(- 1 * b)2 + - 1 * (4 * a * c) = - 1 * (4 * a * c) + (- 1 * b)2"
        by auto
      have f5: "c + a * r2 + - 1 * b * r = a * r2 + c + - 1 * b * r"
        by auto
      have f6: "x0 x1 x2 x3. (x3::real) * x02 + x2 * x0 + x1 = x1 + x3 * x02 + x2 * x0"
        by simp
      have f7: "x1 x2 x3. (discrim x3 x2 x1 < 0) = (¬ 0  discrim x3 x2 x1)"
        by auto
      have f8: "r ra rb. discrim r ra rb = ra2 + - 1 * (4 * r * rb)"
        using discrim_def by auto
      have "¬ 4 * a * c + - 1 * (- 1 * b)2  0"
        using a2 by simp
      then have "a * r2 + c + - 1 * b * r  0"
        using f8 f7 f6 f5 f4 f3 by (metis (no_types) aneq discriminant_negative)
      then show False
        using a1 by linarith
    qed 
    then have "¬(b^2 - 4*a*c < 0)" using root
      using b2 - 4 * a * c < 0  a * r2 + b * r + c  0 by auto
    then have discrim: "b2  4 * a * c " by auto
    then have req: "r = (b + sqrt(b^2 - 4*a*c))/(2*a)  r = (b - sqrt(b^2 - 4*a*c))/(2*a)"
      using aneq root discriminant_iff[where a="a", where b ="-b", where c="c", where x="r"] unfolding discrim_def
      by auto
    then have "r = (b - sqrt(b^2 - 4*a*c))/(2*a)  b > 2*a*r"
    proof - 
      assume req: "r = (b - sqrt(b^2 - 4*a*c))/(2*a)"
      then have h1: "2*a*r = 2*a*((b - sqrt(b^2 - 4*a*c))/(2*a))" by auto
      then have h2: "2*a*((b - sqrt(b^2 - 4*a*c))/(2*a)) = b - sqrt(b^2 - 4*a*c)"
        using aneq by auto
      have h3: "sqrt(b^2 - 4*a*c)  0" using discrim  by auto
      then have "b - sqrt(b^2 - 4*a*c) < b"
        using b_lt h1 h2 by linarith
      then show ?thesis using req h2 by auto
    qed
    then have req: "r = (b + sqrt(b^2 - 4*a*c))/(2*a)" using req b_lt by auto
    then have discrim2: "b^2 - 4 *a*c > 0" using aneq b_lt  by auto
    then have "x y. x  y  a * x2 + b * x + c = 0  a * y2 + b * y + c = 0"
      using aneq discriminant_pos_ex[of a b c] unfolding discrim_def
      by auto
    then obtain x y where xy_prop: "x < y  a * x2 + b * x + c = 0  a * y2 + b * y + c = 0"
      by (meson linorder_neqE_linordered_idom)
    then have "(x = (-b + sqrt(b^2 - 4*a*c))/(2*a)  y = (-b - sqrt(b^2 - 4*a*c))/(2*a))
 (y = (-b + sqrt(b^2 - 4*a*c))/(2*a)  x = (-b - sqrt(b^2 - 4*a*c))/(2*a))" 
      using aneq discriminant_iff unfolding discrim_def by auto   
    then have xy_prop2: "(x = (-b + sqrt(b^2 - 4*a*c))/(2*a)  y = -r)
     (y = (-b + sqrt(b^2 - 4*a*c))/(2*a)  x = -r)" using req
      by (simp add: x = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b - sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  x = (- b - sqrt (b2 - 4 * a * c)) / (2 * a) minus_divide_left)
        (* When a < 0, -r is the bigger root *)
    have alt: "a < 0  k > -r. a * k^2 + b * k + c < 0"
    proof clarsimp 
      fix k
      assume alt: " a < 0"
      assume "- r < k"
      have alt2: " (1/(2*a)::real) < 0" using alt
        by simp 
      have "(-b - sqrt(b^2 - 4*a*c)) < (-b + sqrt(b^2 - 4*a*c))"
        using discrim2 by auto
      then have "(-b - sqrt(b^2 - 4*a*c))* (1/(2*a)::real) > (-b + sqrt(b^2 - 4*a*c))* (1/(2*a)::real)"
        using alt2
        using mult_less_cancel_left_neg by fastforce 
      then have rgtroot: "-r >  (-b + sqrt(b^2 - 4*a*c))/(2*a)"
        using req  x = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b - sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  x = (- b - sqrt (b2 - 4 * a * c)) / (2 * a) xy_prop2
        by auto 
      then have "(y = -r  x = (-b + sqrt(b^2 - 4*a*c))/(2*a))"
        using xy_prop xy_prop2 by auto
      then show "a * k^2 + b * k + c < 0"
        using xy_prop - r < k alt quadratic_shape2b xy_prop 
        by blast 
    qed
      (* When a > 0, -r is the smaller root *)
    have agt: "a > 0  y'>- r. x{-r<..y'}. a * x2 + b * x + c < 0"
    proof - 
      assume agt: "a> 0"
      have alt2: " (1/(2*a)::real) > 0" using agt
        by simp 
      have "(-b - sqrt(b^2 - 4*a*c)) < (-b + sqrt(b^2 - 4*a*c))"
        using discrim2 by auto
      then have "(-b - sqrt(b^2 - 4*a*c))* (1/(2*a)::real) < (-b + sqrt(b^2 - 4*a*c))* (1/(2*a)::real)"
        using alt2
      proof -
        have f1: "- b - sqrt (b2 - c * (4 * a)) < - b + sqrt (b2 - c * (4 * a))"
          by (metis - b - sqrt (b2 - 4 * a * c) < - b + sqrt (b2 - 4 * a * c) mult.commute)
        have "0 < a * 2"
          using 0 < 1 / (2 * a) by auto
        then show ?thesis
          using f1 by (simp add: divide_strict_right_mono mult.commute)
      qed
      then have rlltroot: "-r <  (-b + sqrt(b^2 - 4*a*c))/(2*a)"
        using req x = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b - sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  x = (- b - sqrt (b2 - 4 * a * c)) / (2 * a) xy_prop2
        by auto
      then have "(x = -r  y = (-b + sqrt(b^2 - 4*a*c))/(2*a))"
        using xy_prop xy_prop2 by auto
      have "k. x < k  k < y" using xy_prop dense by auto
      then obtain k where k_prop: "x < k  k < y" by auto
      then have "x{-r<..k}. a * x2 + b * x + c < 0"
        using agt quadratic_shape1a[where a= "a", where b = "b", where c= "c", where x = "x", where y = "y"]
        using x = - r  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a) greaterThanAtMost_iff xy_prop by auto 
      then show "y'>- r. x{-r<..y'}. a * x2 + b * x + c < 0" 
        using k_prop using x = - r  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a) by blast 
    qed
    show ?thesis
      using alt agt
      by (metis aneq greaterThanAtMost_iff less_add_same_cancel1 linorder_neqE_linordered_idom zero_less_one) 
  qed
  show "y'>- r. x{-r<..y'}. a * x2 + b * x + c < 0" using aeq aneq
    by blast 
qed

lemma case_d4:
  fixes a b c r::"real"
  shows "y'. b  2 * a * r 
          ¬ b < 2 * a * r 
          a *r^2 - b * r + c = 0 
          -r < y'  x{-r<..y'}. ¬ a * x2 + b * x + c < 0"
proof - 
  fix y'
  assume bneq: "b  2 * a * r"
  assume bnotless: "¬ b < 2 * a * r"
  assume root: "a *r^2 - b * r + c = 0"
  assume y_prop: "-r < y'"
  have b_gt: "b > 2*a*r" using bneq bnotless by auto
  have aeq: "a = 0  y'>- r. x{-r<..y'}. a * x2 + b * x + c > 0"
  proof - 
    assume azer: "a = 0"
    then have bgt: "b > 0" using b_gt by auto
    then have "c = b*r" using azer root by auto
    then have eval: "x. a*x^2 + b*x + c = b*(x + r)" using azer
      by (simp add: distrib_left) 
    have "x > -r. b*(x + r) > 0" 
    proof clarsimp 
      fix x
      assume xgt: "- r < x"
      then have "x + r > 0"
        by linarith 
      then show "b * (x + r) > 0"
        using bgt by auto 
    qed
    then show ?thesis using eval 
      using less_add_same_cancel1 zero_less_one
      by (metis greaterThanAtMost_iff) 
  qed
  have aneq: "a  0 y'>- r. x{-r<..y'}. a * x2 + b * x + c > 0"
  proof - 
    assume aneq: "a0"  
    {
      assume a1: "a * r2 - b * r + c = 0"
      assume a2: "b2 < 4 * a * c"
      have f3: "(0  - 1 * (4 * a * c) + (- 1 * b)2) = (4 * a * c + - 1 * (- 1 * b)2  0)"
        by simp
      have f4: "(- 1 * b)2 + - 1 * (4 * a * c) = - 1 * (4 * a * c) + (- 1 * b)2"
        by auto
      have f5: "c + a * r2 + - 1 * b * r = a * r2 + c + - 1 * b * r"
        by auto
      have f6: "x0 x1 x2 x3. (x3::real) * x02 + x2 * x0 + x1 = x1 + x3 * x02 + x2 * x0"
        by simp
      have f7: "x1 x2 x3. (discrim x3 x2 x1 < 0) = (¬ 0  discrim x3 x2 x1)"
        by auto
      have f8: "r ra rb. discrim r ra rb = ra2 + - 1 * (4 * r * rb)"
        using discrim_def by auto
      have "¬ 4 * a * c + - 1 * (- 1 * b)2  0"
        using a2 by simp
      then have "a * r2 + c + - 1 * b * r  0"
        using f8 f7 f6 f5 f4 f3 by (metis (no_types) aneq discriminant_negative)
      then have False
        using a1 by linarith
    } note * = this
    have "b^2 - 4*a*c < 0  a * r2 + b * r + c  0" using root discriminant_negative[of a b c r] unfolding discrim_def 
      using aneq by auto
    then have "¬(b^2 - 4*a*c < 0)" using root * by auto
    then have discrim: "b2  4 * a * c " by auto
    then have req: "r = (b + sqrt(b^2 - 4*a*c))/(2*a)  r = (b - sqrt(b^2 - 4*a*c))/(2*a)"
      using aneq root discriminant_iff[where a="a", where b ="-b", where c="c", where x="r"] unfolding discrim_def
      by auto
    then have "r = (b + sqrt(b^2 - 4*a*c))/(2*a)  b < 2*a*r"
    proof - 
      assume req: "r = (b + sqrt(b^2 - 4*a*c))/(2*a)"
      then have h1: "2*a*r = 2*a*((b + sqrt(b^2 - 4*a*c))/(2*a))" by auto
      then have h2: "2*a*((b + sqrt(b^2 - 4*a*c))/(2*a)) = b + sqrt(b^2 - 4*a*c)"
        using aneq by auto
      have h3: "sqrt(b^2 - 4*a*c)  0" using discrim  by auto
      then have "b + sqrt(b^2 - 4*a*c) > b"
        using b_gt h1 h2 by linarith
      then show ?thesis using req h2 by auto
    qed
    then have req: "r = (b - sqrt(b^2 - 4*a*c))/(2*a)" using req b_gt
      using aneq discrim by auto
    then have discrim2: "b^2 - 4 *a*c > 0" using aneq b_gt  by auto
    then have "x y. x  y  a * x2 + b * x + c = 0  a * y2 + b * y + c = 0"
      using aneq discriminant_pos_ex[of a b c] unfolding discrim_def
      by auto
    then obtain x y where xy_prop: "x < y  a * x2 + b * x + c = 0  a * y2 + b * y + c = 0"
      by (meson linorder_neqE_linordered_idom)
    then have "(x = (-b + sqrt(b^2 - 4*a*c))/(2*a)  y = (-b - sqrt(b^2 - 4*a*c))/(2*a))
 (y = (-b + sqrt(b^2 - 4*a*c))/(2*a)  x = (-b - sqrt(b^2 - 4*a*c))/(2*a))" 
      using aneq discriminant_iff unfolding discrim_def by auto   
    then have xy_prop2: "(x = (-b - sqrt(b^2 - 4*a*c))/(2*a)  y = -r)
     (y = (-b - sqrt(b^2 - 4*a*c))/(2*a)  x = -r)" using req divide_inverse minus_diff_eq mult.commute mult_minus_right
      by (smt (verit, ccfv_SIG) uminus_add_conv_diff)
        (* When a > 0, -r is the greater root *)
    have agt: "a > 0  k > -r. a * k^2 + b * k + c > 0"
    proof clarsimp 
      fix k
      assume agt: " a > 0"
      assume "- r < k"
      have agt2: " (1/(2*a)::real) > 0" using agt
        by simp 
      have "(-b - sqrt(b^2 - 4*a*c)) < (-b + sqrt(b^2 - 4*a*c))"
        using discrim2 by auto
      then have "(-b - sqrt(b^2 - 4*a*c))* (1/(2*a)::real) < (-b + sqrt(b^2 - 4*a*c))* (1/(2*a)::real)"
        using agt2 by (simp add: divide_strict_right_mono) 
      then have rgtroot: "-r >  (-b - sqrt(b^2 - 4*a*c))/(2*a)"
        using  req x = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b - sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  x = (- b - sqrt (b2 - 4 * a * c)) / (2 * a) xy_prop2
        by auto 
      then have "(x = (-b - sqrt(b^2 - 4*a*c))/(2*a))  y = -r"
        using xy_prop xy_prop2 
        by auto
      then show "a * k^2 + b * k + c > 0"
        using - r < k xy_prop agt quadratic_shape1b[where a= "a", where b ="b", where c="c", where x = "x", where y = "-r", where z = "k"]    
        by blast 
    qed
      (* When a < 0, -r is the smaller root *)
    have agt2: "a < 0  y'>- r. x{-r<..y'}. a * x2 + b * x + c > 0"
    proof - 
      assume alt: "a<0"
      have alt2: " (1/(2*a)::real) < 0" using alt
        by simp 
      have "(-b - sqrt(b^2 - 4*a*c)) < (-b + sqrt(b^2 - 4*a*c))"
        using discrim2 by auto
      then have "(-b - sqrt(b^2 - 4*a*c))* (1/(2*a)::real) > (-b + sqrt(b^2 - 4*a*c))* (1/(2*a)::real)"
        using alt2  using mult_less_cancel_left_neg by fastforce 
      then have rlltroot: "-r < (-b - sqrt(b^2 - 4*a*c))/(2*a)"
        using req 
        using x = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b - sqrt (b2 - 4 * a * c)) / (2 * a)  y = (- b + sqrt (b2 - 4 * a * c)) / (2 * a)  x = (- b - sqrt (b2 - 4 * a * c)) / (2 * a) 
          xy_prop2 
        by auto
      then have h: "(x = -r  y = (-b - sqrt(b^2 - 4*a*c))/(2*a))"
        using xy_prop xy_prop2 
        by auto
      have "k. x < k  k < y" using xy_prop dense by auto
      then obtain k where k_prop: "x < k  k < y" by auto
      then have "x{-r<..k}. a * x2 + b * x + c > 0"
        using alt quadratic_shape2a[where a= "a", where b = "b", where c= "c", where x = "x", where y = "y"]
          xy_prop  h greaterThanAtMost_iff  by auto 
      then show "y'>- r. x{-r<..y'}. a * x2 + b * x + c > 0" 
        using k_prop using h by blast 
    qed
    show ?thesis
      using aneq agt agt2
      by (meson greaterThanAtMost_iff linorder_neqE_linordered_idom y_prop) 
  qed
  show "x{-r<..y'}. ¬ a * x2 + b * x + c < 0" using aneq aeq
    by (metis greaterThanAtMost_iff less_eq_real_def linorder_not_less y_prop)
qed

lemma one_root_a_lt0:
  fixes a b c r y'::"real"
  assumes alt: "a < 0"
  assumes beq: "b = 2 * a * r"
  assumes root: " a * r^2 - 2*a*r*r + c = 0"
  shows "y'>- r. x{- r<..y'}. a * x2 + 2*a*r*x + c < 0"
proof - 
  have root_iff: "x. a * x2 + b * x + c = 0  x = -r" using alt root discriminant_lemma[where r = "r"] beq 
    by auto
  have "a < 0  (y. x > y. a*x^2 + b*x + c < 0)" using neg_lc_dom_quad 
    by auto
  then obtain k where k_prop: "x > k. a*x^2 + b*x + c < 0" using alt by auto
  let ?mx = "max (k+1) (-r + 1)"
  have "a*?mx^2 + b*?mx + c < 0" using k_prop by auto
  then have "y > -r. a*y^2 + b*y + c < 0"
    by force
  then obtain z where z_prop: "z > -r  a*z^2 + b*z + c < 0" by auto
  have poly_eval_prop: "(x::real). poly [:c, b, a :] x = a*x^2 + b*x + c" 
    using quadratic_poly_eval by auto
  then have nozer: "¬(x. (x > -r  poly [:c, b, a :] x = 0))" using root_iff 
    by (simp add: add.commute) 
  have poly_z: "poly [:c, b, a:] z < 0" using z_prop poly_eval_prop by auto
  have "y > -r. a*y^2 + b*y + c < 0" 
  proof clarsimp 
    fix y
    assume ygt: "- r < y"
    have h1: "y = z  a * y2 + b * y + c < 0" using z_prop by auto
    have h2: "y < z  a * y2 + b * y + c < 0" proof -
      assume ylt: "y < z"
      have notz: "a*y^2 + b*y + c  0" using ygt nozer poly_eval_prop by auto
      have h1: "a *y^2 + b*y + c > 0  poly [:c, b, a:] y > 0" using poly_eval_prop by auto
      have ivtprop: "poly [:c, b, a:] y > 0  (x. y < x  x < z  poly [:c, b, a:] x = 0)" 
        using ylt poly_z poly_IVT_neg[where a = "y", where b = "z", where p = "[:c, b, a:]"]
        by auto
      then have "a*y^2 + b*y + c > 0  False" using h1 ivtprop ygt nozer by auto
      then show "a*y^2 + b*y + c < 0" using notz
        using linorder_neqE_linordered_idom by blast 
    qed
    have h3: "y > z  a * y2 + b * y + c < 0" 
    proof -
      assume ygtz: "y > z"
      have notz: "a*y^2 + b*y + c  0" using ygt nozer poly_eval_prop by auto
      have h1: "a *y^2 + b*y + c > 0  poly [:c, b, a:] y > 0" using poly_eval_prop by auto
      have ivtprop: "poly [:c, b, a:] y > 0  (x. z < x  x < y  poly [:c, b, a:] x = 0)" 
        using ygtz poly_z using poly_IVT_pos by blast 
      then have "a*y^2 + b*y + c > 0  False" using h1 ivtprop z_prop nozer by auto
      then show "a*y^2 + b*y + c < 0" using notz
        using linorder_neqE_linordered_idom by blast 
    qed
    show "a * y2 + b * y + c < 0" using h1 h2 h3
      using linorder_neqE_linordered_idom by blast
  qed
  then show ?thesis
    using y>- r. a * y2 + b * y + c < 0 beq by auto 
qed


lemma one_root_a_lt0_var:
  fixes a b c r y'::"real"
  assumes alt: "a < 0"
  assumes beq: "b = 2 * a * r"
  assumes root: " a * r^2 - 2*a*r*r + c = 0"
  shows "y'>- r. x{- r<..y'}. a * x2 + 2*a*r*x + c  0"
proof - 
  have h1: "y'>- r. x{- r<..y'}. a * x2 + 2 * a * r * x + c < 0 
     y'>-r. x{- r<..y'}. a * x2 + 2 * a *r * x + c  0"
    using less_eq_real_def by blast
  then show ?thesis
    using one_root_a_lt0[of a b r] assms by auto
qed

subsection "More Continuity Properties"
lemma continuity_lem_gt0_expanded_var: 
  fixes r:: "real"
  fixes a b c:: "real"
  fixes k::"real"
  assumes kgt: "k > r"
  shows "a*r^2 + b*r + c > 0 
    x{r<..k}. a*x^2 + b*x + c  0"
proof -
  assume a: "a*r^2 + b*r + c > 0  "
  have h: "x{r<..k}. a*x^2 + b*x + c > 0   x{r<..k}. a*x^2 + b*x + c  0"
    using less_eq_real_def by blast 
  have "x{r<..k}. a*x^2 + b*x + c > 0" using a continuity_lem_gt0_expanded[of r k a b c] assms by auto
  then show "x{r<..k}. a*x^2 + b*x + c  0"
    using h by auto
qed

lemma continuity_lem_lt0_expanded_var: 
  fixes r:: "real"
  fixes a b c:: "real"
  shows "a*r^2 + b*r + c < 0 
    y'> r. x{r<..y'}. a*x^2 + b*x + c  0"
proof - 
  assume "a*r^2 + b*r + c < 0 "
  then have " y'> r. x{r<..y'}. a*x^2 + b*x + c < 0"
    using continuity_lem_lt0_expanded by auto
  then show " y'> r. x{r<..y'}. a*x^2 + b*x + c  0"
    using less_eq_real_def by auto
qed

lemma nonzcoeffs:
  fixes a b c r::"real"
  shows "a0  b0  c0  y'>r. x{r<..y'}. a * x2 + b * x + c  0 "
proof - 
  assume "a0  b0  c0"
  then have fin: "finite {x. a*x^2 + b*x + c = 0}"
    by (metis pCons_eq_0_iff poly_roots_finite poly_roots_set_same) 
      (* then have fin2: "finite {x. a*x^2 + b*x + c = 0 ∧ x > r}"
    using finite_Collect_conjI by blast *)
  let ?s = "{x. a*x^2 + b*x + c = 0}"
  have imp: "(q  ?s. q > r)  (q  ?s. (q > r  (x  ?s. x > r  x  q)))"
  proof - 
    assume asm: "(q  ?s. q > r)"
    then have none: "{q. q  ?s  q > r}  {}"
      by blast 
    have fin2: "finite {q. q  ?s  q > r}" using fin
      by simp
    have "k. k = Min  {q. q  ?s  q > r}" using fin2 none
      by blast
    then obtain k where k_prop: "k =  Min  {q. q  ?s  q > r}" by auto
    then have kp1: "k  ?s  k > r" 
      using Min_in fin2 none
      by blast 
    then  have kp2: "x  ?s. x > r  x  k" 
      using Min_le fin2  using k_prop by blast 
    show "(q  ?s. (q > r  (x  ?s. x > r  x  q)))" 
      using kp1 kp2 by blast
  qed
  have h2: "(q  ?s. q > r)  y'>r. x{r<..y'}. a * x2 + b * x + c  0" 
  proof - 
    assume "(q  ?s. q > r)"
    then obtain q where q_prop: "q  ?s  (q > r  (x  ?s. x > r  x  q))"
      using imp by blast 
    then have "w. w > r  w < q" using dense
      by blast
    then obtain w where w_prop: "w > r  w < q" by auto
    then have "¬(x{r<..w}. x  ?s)"
      using w_prop q_prop by auto
    then have "x{r<..w}. a * x2 + b * x + c  0"
      by blast
    then show "y'>r. x{r<..y'}. a * x2 + b * x + c  0"
      using w_prop by blast
  qed
  have h1: "¬(q  ?s. q > r)  y'>r. x{r<..y'}. a * x2 + b * x + c  0"
  proof - 
    assume "¬(q  ?s. q > r)"
    then have "x{r<..(r+1)}. a * x2 + b * x + c  0"
      using greaterThanAtMost_iff by blast
    then show ?thesis
      using less_add_same_cancel1 less_numeral_extra(1) by blast 
  qed
  then show "y'>r. x{r<..y'}. a * x2 + b * x + c  0"
    using h2 by blast
qed


(* Show if there are infinitely many values of x where a*x^2 + b*x + c is 0,
then the a*x^2 + b*x + c is the zero polynomial *)
lemma infzeros : 
  fixes y:: "real"
  assumes "x::real < (y::real). a * x2 + b * x + c = 0"
  shows "a = 0  b=0  c=0"
proof - 
  let ?A = "{(x::real). x < y}"
  have " (n::nat) f. ?A = f ` {i. i < n}  inj_on f {i. i < n}  False"
  proof clarsimp 
    fix n:: "nat" 
    fix f
    assume xlt: "{x. x < y} = f ` {i. i < n}"
    assume injh: "inj_on f {i. i < n}"
    have "?A  {}"
      by (simp add: linordered_field_no_lb)
    then have ngtz: "n > 0" 
      using xlt injh using gr_implies_not_zero by auto 
    have cardisn: "card ?A = n" using xlt injh
      by (simp add: card_image) 
    have "k::nat. ((y - (k::nat) - 1)  ?A)" 
      by auto
    then have subs: "{k. (x::nat). k = y - x - 1  0  x  x  n}  ?A"
      by auto
    have seteq: "(λx. y - real x - 1) ` {0..n} ={k. (x::nat). k = y - x - 1  0  x  x  n}"
      by auto
    have injf: "inj_on (λx. y - real x - 1) {0..n}"
      unfolding inj_on_def by auto
    have "card {k. (x::nat). k = y - x - 1  0  x  x  n} = n + 1"
      using  injf seteq card_atMost inj_on_iff_eq_card[where A = "{0..n}", where f = "λx. y - x - 1"] 
      by auto
    then have if_fin: "finite ?A  card ?A  n + 1" 
      using subs card_mono
      by (metis (lifting) card_mono)
    then have if_inf: "infinite ?A  card ?A = 0"
      by (meson card.infinite)
    then show "False" using if_fin if_inf cardisn ngtz by auto
  qed
  then have nfin: "¬ finite {(x::real). x < y}"
    using finite_imp_nat_seg_image_inj_on by blast
  have "{(x::real). x < y}  {x. a*x^2 + b*x + c = 0}"
    using assms by auto
  then have nfin2: "¬ finite {x. a*x^2 + b*x + c = 0}"
    using nfin finite_subset by blast 
  {
    fix x
    assume "a * x2 + b * x + c = 0"
    then have f1: "a * (x * x) + x * b + c = 0"
      by (simp add: Groups.mult_ac(2) power2_eq_square)
    have f2: "r. c + (r + (c + - c)) = r + c"
      by simp
    have f3: "r ra rb. (rb::real) * ra + ra * r = (rb + r) * ra"
      by (metis Groups.mult_ac(2) Rings.ring_distribs(2))
    have "r. r + (c + - c) = r"
      by simp
    then have "c + x * (b + x * a) = 0"
      using f3 f2 f1 by (metis Groups.add_ac(3) Groups.mult_ac(1) Groups.mult_ac(2))
  }
  hence "{x. a*x^2 + b*x + c = 0}  {x. poly [:c, b, a:] x = 0}"
    by auto
  then have " ¬ finite {x. poly [:c, b, a:] x = 0}" 
    using nfin2 using finite_subset by blast 
  then have "[:c, b, a:] = 0" 
    using poly_roots_finite[where p = "[:c, b, a:]"]  by auto
  then show ?thesis
    by auto
qed



lemma have_inbetween_point_leq:
  fixes r::"real"
  assumes "(((d::real), (e::real), (f::real))set leq. y'>r. x{r<..y'}. d * x2 + e * x + f  0)"
  shows "(x. ((a, b, c)set leq. a * x2 + b * x + c  0))"
proof -
  have "((d, e, f)set leq. y'>r. x{r<..y'}. d * x2 + e * x + f  0)  
    (y'>r. ((d, e, f)set leq. x{r<..y'}. d * x2 + e * x + f  0))"
    using leq_qe_inf_helper assms by auto
  then have "(y'>r. ((d, e, f)set leq. x{r<..y'}. d * x2 + e * x + f  0))"
    using assms
    by blast 
  then obtain y where y_prop: "y > r   ((d, e, f)set leq. x{r<..y}. d * x2 + e * x + f  0)"
    by auto
  have "q. q >  r q < y" using y_prop dense by auto
  then obtain q where q_prop: "q > r  q < y" by auto
  then have "((d, e, f)set leq. d*q^2 + e*q + f  0)"
    using y_prop by auto
  then show ?thesis
    by auto
qed


lemma have_inbetween_point_neq:
  fixes r::"real"
  assumes "(((d::real), (e::real), (f::real))set neq. y'>r. x{r<..y'}. d * x2 + e * x + f  0)"
  shows "(x. ((a, b, c)set neq. a * x2 + b * x + c  0))"
proof -
  have "((d, e, f)set neq. y'>r. x{r<..y'}. d * x2 + e * x + f  0)  
    (y'>r. ((d, e, f)set neq. x{r<..y'}. d * x2 + e * x + f  0))"
    using neq_qe_inf_helper assms by auto
  then have "(y'>r. ((d, e, f)set neq. x{r<..y'}. d * x2 + e * x + f  0))"
    using assms
    by blast 
  then obtain y where y_prop: "y > r   ((d, e, f)set neq. x{r<..y}. d * x2 + e * x + f  0)"
    by auto
  have "q. q >  r q < y" using y_prop dense by auto
  then obtain q where q_prop: "q > r  q < y" by auto
  then have "((d, e, f)set neq. d*q^2 + e*q + f  0)"
    using y_prop by auto
  then show ?thesis
    by auto
qed

subsection "Setting up and Helper Lemmas"
subsubsection "The les\\_qe lemma"
lemma les_qe_forward : 
  shows "((((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0)))))  ((x. ((a, b, c)set les. a * x2 + b * x + c < 0)))"
proof -
  assume big_asm: "((((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0)))))"
  then have big_or: "((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  
               ((a', b', c')set les.
               a' = 0 
               b'  0  ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0)) 
        
        ((a', b', c')set les.
               a'  0 
               4 * a' * c'  b'2 
               ((d, e, f)set les.
                   y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                      x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)) 
      
      ((a', b', c')set les.  a'  0 
               4 * a' * c'  b'2 
                ((d, e, f)set les.
                    y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                       x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                          d * x2 + e * x + f < 0)) " 
    by auto
  have h1_helper: "((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  (y.x<y. ((a, b, c)set les. a * x2 + b * x + c < 0))"
  proof - 
    show "((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  (y.x<y. ((a, b, c)set les. a * x2 + b * x + c < 0))" 
    proof (induct les)
      case Nil
      then show ?case
        by auto
    next
      case (Cons q les) 
      have ind: " aset (q # les). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0"
        using Cons.prems
        by auto
      then have "case q of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0 "
        by simp      
      then obtain y2 where y2_prop: "case q of (a, ba, c)   (y<y2. a * y2 + ba * y + c < 0)"
        by auto
      have "aset les. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0"
        using ind by simp
      then have " y. x<y. aset les. case a of (a, ba, c)  a * x2 + ba * x + c < 0"
        using Cons.hyps by blast 
      then obtain y1 where y1_prop: "x<y1. aset les. case a of (a, ba, c)  a * x^2 + ba * x + c < 0"
        by blast
      let ?y = "min y1 y2"
      have "x < ?y.  (aset (q #les). case a of (a, ba, c)  a * x^2 + ba * x + c < 0)"
        using y1_prop y2_prop 
        by fastforce 
      then show ?case
        by blast 
    qed
  qed
  then have h1: "((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) (x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
    by (smt (z3) infzeros less_eq_real_def not_numeral_le_zero)
      (* apply (auto)
    by (metis (lifting) infzeros zero_neq_numeral) *)
  have h2: " ((a', b', c')set les.
               a' = 0 
               b'  0  ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0))
     (x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
  proof -
    assume asm: "((a', b', c')set les. a' = 0  b'  0 
         ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0))"
    then obtain a' b' c' where abc_prop: "(a', b', c') set les  a' = 0  b'  0 
         ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0)"
      by auto
    then show "(x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
      using have_inbetween_point_les by auto
  qed
  have h3: " ((a', b', c')set les.
               a'  0 
               4 * a' * c'  b'2 
               ((d, e, f)set les.
                   y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                      x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0))  ((x. ((a, b, c)set les. a * x2 + b * x + c < 0)))"
  proof - 
    assume asm: "(a', b', c')set les.  a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
                y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                   x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                      d * x2 + e * x + f < 0)"
    then obtain a' b' c' where abc_prop: "(a', b', c')set les  a'  0  4 * a' * c'  b'2 
       ((d, e, f)set les.
           y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
              x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)"
      by auto
    then show "(x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
      using have_inbetween_point_les by auto
  qed
  have h4: "((a', b', c')set les.  a'  0 
               4 * a' * c'  b'2 
                ((d, e, f)set les.
                    y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                       x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                          d * x2 + e * x + f < 0))  (x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
  proof - 
    assume asm: "((a', b', c')set les.  a'  0 
         4 * a' * c'  b'2 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0)) "
    then obtain a' b' c' where abc_prop: "(a', b', c')set les  a'  0  4 * a' * c'  b'2 
     ((d, e, f)set les.
         y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
            x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}. d * x2 + e * x + f < 0)"
      by auto
    then have "(x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
      using have_inbetween_point_les by auto
    then show ?thesis using asm by auto
  qed 
  show ?thesis using big_or h1 h2 h3 h4
    by blast 
qed

(*sample points, some starter proofs below in comments *)
lemma les_qe_backward : 
  shows "(x. ((a, b, c)set les. a * x2 + b * x + c < 0)) 
    (((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))"

proof - 
  assume havex: "(x. ((a, b, c)set les. a * x2 + b * x + c < 0))"
  then obtain x where x_prop: "(a, b, c)set les. a * x2 + b * x + c < 0" by auto
  have h: "(¬ ((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  ¬ ((a', b', c')set les.
           a' = 0 
           b'  0 
           ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0)) 
        ¬ ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                  x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)) 
        ¬ ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                  x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}. d * x2 + e * x + f < 0)))  False"
  proof -
    assume big: "(¬ ((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  ¬ ((a', b', c')set les.
           a' = 0 
           b'  0 
           ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0)) 
        ¬ ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                  x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)) 
        ¬ ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                  x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}. d * x2 + e * x + f < 0)))"
    have notneginf: "¬ ((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)" using big by auto
    have notlinroot: "¬ ((a', b', c')set les.
           a' = 0 
           b'  0 
           ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0))" 
      using big by auto
    have notquadroot1: " ¬ ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                  x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0))"
      using big by auto
    have notquadroot2:" ¬ ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                  x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}. d * x2 + e * x + f < 0))"
      using big by auto
    have nok: "¬ (k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))"
    proof - 
      have "(k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))  False"
      proof - 
        assume "(k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))"
        then obtain k a b c where k_prop: "(a, b, c)  set les   a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0)"
          by auto
        have azer:  "a = 0  False"
        proof - 
          assume azer: "a = 0"
          then have "b = 0  c = 0" using k_prop by auto
          then have bnonz: "b 0"
            using azer x_prop k_prop 
            by auto 
          then have "k = -c/b" using k_prop azer
            by (metis (no_types, hide_lams) add.commute add.left_neutral add_uminus_conv_diff diff_le_0_iff_le divide_non_zero less_eq_real_def mult_zero_left neg_less_iff_less order_less_irrefl real_add_less_0_iff)
          then have " ((a', b', c')set les.
           a' = 0  b'  0  ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0))"
            using k_prop azer bnonz by auto
          then show "False" using notlinroot
            by auto
        qed
        have anonz: "a  0  False"
        proof - 
          assume anonz: "a  0 "
          let ?r1 = "(- b - sqrt (b^2 - 4 * a * c)) / (2 * a)"
          let ?r2 = "(- b + sqrt (b^2 - 4 * a * c)) / (2 * a)"
          have discr: "4 * a * c  b^2" using anonz k_prop discriminant_negative[of a b c] 
            unfolding discrim_def 
            by fastforce 
          then have "k = ?r1  k = ?r2" using k_prop discriminant_nonneg[of a b c] unfolding discrim_def
            using anonz
            by auto 
          then have "((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                  x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)) 
           ((a', b', c')set les.
           a'  0 
           4 * a' * c'  b'2 
           ((d, e, f)set les.
               y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                  x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}. d * x2 + e * x + f < 0))"
            using discr anonz notquadroot1 notquadroot2 k_prop 
            by auto
          then show "False" using  notquadroot1 notquadroot2
            by auto
        qed
        show "False"
          using azer anonz  by auto
      qed
      then show ?thesis by auto
    qed
    have finset: "finite (set les)"
      by blast
    have h1: "((a, b, c)set les. a = 0  b = 0  c = 0)   False"
      using x_prop by fastforce
    then have h2: "¬((a, b, c)set les. a = 0  b = 0  c = 0)  False"
    proof - 
      assume nozer: "¬((a, b, c)set les. a = 0  b = 0  c = 0)"
      then have same_set: "root_set (set les) = set (sorted_root_list_set (set les))"
        using root_set_finite finset set_sorted_list_of_set
        by (simp add: nozer root_set_finite sorted_root_list_set_def)
      have xnotin: "x  root_set (set les)"
        unfolding root_set_def using x_prop by auto
      let ?srl = "sorted_root_list_set (set les)"
      have notinlist: "¬ List.member ?srl x"
        using xnotin same_set
        by (simp add: in_set_member)
      then have notmem: "n < (length ?srl). x  nth_default 0 ?srl n"
        using nth_mem same_set xnotin nth_default_def
        by metis  
      show ?thesis 
      proof (induct ?srl)
        case Nil
        then have "((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)"
        proof clarsimp 
          fix a b c
          assume noroots: "[] = sorted_root_list_set (set les)"
          assume inset: "(a, b, c)  set les"
          have "{} = root_set (set les)" 
            using noroots same_set 
            by auto 
          then have nozero: "¬(x. a*x^2  + b*x + c = 0)"
            using inset unfolding root_set_def by auto
          have "y<x. a * y2 + b * y + c < 0" 
          proof clarsimp 
            fix y
            assume "y < x"
            then have "sign_num (a*x^2 + b*x + c) = sign_num (a*y^2 + b*y + c)"
              using nozero  by (metis changes_sign_var) 
            then show "a * y2 + b * y + c < 0"
              unfolding sign_num_def using x_prop inset 
              by (smt split_conv) 
          qed
          then show "x. y<x. a * y2 + b * y + c < 0"
            by auto
        qed
        then show ?case using notneginf by auto
      next
        case (Cons w xa) 
          (* Need to argue that x isn't greater than the largest element of ?srl *)
          (* that if srl has length ≥ 2, x isn't in between any of the roots of ?srl*)
          (* and that x isn't less than the lowest root in ?srl *)
        then have lengthsrl: "length ?srl > 0" by auto
        have neginf: "x < nth_default 0 ?srl 0  False"
        proof -
          assume xlt: "x < nth_default 0 ?srl 0"
          have all: "((a, b, c)set les. y<x. a * y2 + b * y + c < 0)"
          proof clarsimp 
            fix a b c y
            assume inset: "(a, b, c)  set les"
            assume "y < x"
            have xl: "a*x^2 + b*x + c < 0" using x_prop inset by auto
            have "¬(q. q < nth_default 0 ?srl 0   a*q^2 + b*q + c = 0)"
            proof - 
              have "(q. q < nth_default 0 ?srl 0   a*q^2 + b*q + c = 0)  False"
              proof - assume "q. q < nth_default 0 ?srl 0   a*q^2 + b*q + c = 0"
                then obtain q where q_prop: "q < nth_default 0 ?srl 0 a*q^2 + b*q + c = 0" by auto
                then have " q  root_set (set les)" unfolding root_set_def using inset by auto
                then have "List.member ?srl q" using same_set
                  by (simp add: in_set_member)
                then have "q  nth_default 0 ?srl 0"
                  using sorted_sorted_list_of_set[where A = "root_set (set les)"]
                  unfolding sorted_root_list_set_def
                  by (metis q  root_set (set les) in_set_conv_nth le_less_linear lengthsrl not_less0 nth_default_nth same_set sorted_nth_mono sorted_root_list_set_def)
                then show "False" using q_prop by auto
              qed
              then show ?thesis by auto
            qed
            then have "¬(q. q < x  a*q^2 + b*q + c = 0)" using xlt by auto
            then show " a * y2 + b * y + c < 0" 
              using xl changes_sign_var[where a = "a", where b = "b", where c = "c", where x = "y", where y = "x"]
              unfolding sign_num_def using y < x less_eq_real_def zero_neq_numeral 
              by fastforce
          qed
          have "((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)"
          proof clarsimp 
            fix a b c
            assume "(a, b, c)set les"
            then show "x. y<x. a * y2 + b * y + c < 0" 
              using all by blast 
          qed
          then show "False" using notneginf by auto
        qed
        have "x > nth_default 0 ?srl (length ?srl - 1)  (k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))"
        proof - 
          assume xgt: "x > nth_default 0 ?srl (length ?srl - 1)"
          let ?lg = "nth_default 0 ?srl (length ?srl - 1)"
          have "List.member ?srl ?lg"
            by (metis diff_less in_set_member lengthsrl nth_default_def nth_mem zero_less_one)
          then have "?lg  root_set (set les) "
            using same_set in_set_member[of ?lg ?srl]  by auto
          then have exabc: "(a, b, c)set les. a*?lg^2 + b*?lg + c = 0"
            unfolding root_set_def by auto
          have "((d, e, f)set les. q{?lg<..x}. d * q^2 + e * q + f < 0)"
          proof clarsimp 
            fix d e f q 
            assume inset: "(d, e, f)  set les"
            assume qgt: "(nth_default 0) (sorted_root_list_set (set les)) (length (sorted_root_list_set (set les)) - Suc 0) < q"
            assume qlt: "q  x"
            have nor: "¬(r. d * r^2 + e * r + f = 0  r > ?lg)"
            proof - 
              have "(r. d * r^2 + e * r + f = 0  r > ?lg)  False "
              proof - 
                assume "r. d * r^2 + e * r + f = 0  r > ?lg"
                then obtain r where r_prop: "d*r^2 + e*r + f = 0  r > ?lg" by auto
                then have "r  root_set (set les)" using inset unfolding root_set_def by auto
                then have "List.member ?srl r"
                  using same_set in_set_member
                  by (simp add: in_set_member) 
                then have " r  ?lg" using sorted_sorted_list_of_set nth_default_def
                  by (metis One_nat_def Suc_pred r  root_set (set les) in_set_conv_nth lengthsrl lessI less_Suc_eq_le same_set sorted_nth_mono sorted_root_list_set_def)
                then show "False" using r_prop by auto
              qed
              then show ?thesis by auto
            qed
            then have xltz_helper: "¬(r. r  q  d * r^2 + e * r + f = 0)"
              using qgt by auto
            then have xltz: "d*x^2 + e*x + f < 0" using inset x_prop by auto
            show "d * q2 + e * q + f < 0"
              using qlt qgt nor changes_sign_var[of d _ e f _] xltz xltz_helper unfolding sign_num_def
              apply (auto) 
              by smt
          qed
          then have " ((d, e, f)set les. y'>?lg. x{?lg<..y'}. d * x2 + e * x + f < 0)"
            using xgt by auto
          then have "((a, b, c)set les. a*?lg^2 + b*?lg + c = 0 
                ((d, e, f)set les. y'>?lg. x{?lg<..y'}. d * x2 + e * x + f < 0))"
            using exabc by auto
          then show "(k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))"
            by auto
        qed
        then have posinf: "x > nth_default 0 ?srl (length ?srl - 1)  False" 
          using nok by auto
        have "(n. (n+1) < (length ?srl)  x > (nth_default 0 ?srl) n  x < (nth_default 0 ?srl (n + 1)))  (k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))"
        proof - 
          assume "n. (n+1) < (length ?srl)  x > nth_default 0 ?srl n  x < nth_default 0 ?srl (n + 1)"
          then obtain n where n_prop: "(n+1) < (length ?srl)  x > nth_default 0 ?srl n  x < nth_default 0 ?srl (n + 1)" by auto
          let ?elt = "nth_default 0 ?srl n"
          let ?elt2 = "nth_default 0 ?srl (n + 1)"
          have "List.member ?srl ?elt"
            using n_prop nth_default_def
            by (metis add_lessD1 in_set_member nth_mem) 
          then have "?elt  root_set (set les) "
            using same_set in_set_member[of ?elt ?srl]  by auto
          then have exabc: "(a, b, c)set les. a*?elt^2 + b*?elt + c = 0"
            unfolding root_set_def by auto
          then obtain a b c where "(a, b, c)set les  a*?elt^2 + b*?elt + c = 0"
            by auto
          have xltel2: "x < ?elt2" using n_prop by auto
          have xgtel: "x > ?elt " using n_prop by auto
          have "((d, e, f)set les. q{?elt<..x}. d * q^2 + e * q + f < 0)"
          proof clarsimp 
            fix d e f q 
            assume inset: "(d, e, f)  set les"
            assume qgt: "nth_default 0 (sorted_root_list_set (set les)) n < q"
            assume qlt: "q  x"

            have nor: "¬(r. d * r^2 + e * r + f = 0  r > ?elt r < ?elt2)"
            proof - 
              have "(r. d * r^2 + e * r + f = 0  r > ?elt  r < ?elt2)  False "
              proof - 
                assume "r. d * r^2 + e * r + f = 0  r > ?elt   r < ?elt2"
                then obtain r where r_prop: "d*r^2 + e*r + f = 0  r > ?elt   r < ?elt2" by auto
                then have "r  root_set (set les)" using inset unfolding root_set_def by auto
                then have "List.member ?srl r"
                  using same_set in_set_member
                  by (simp add: in_set_member) 
                then have "i < (length ?srl). r = nth_default 0 ?srl i"
                  by (metis r  root_set (set les) in_set_conv_nth same_set nth_default_def)
                then obtain i where i_prop: "i < (length ?srl)  r = nth_default 0 ?srl i"
                  by auto
                have "r > ?elt" using r_prop by auto
                then  have igt: " i > n" using i_prop sorted_sorted_list_of_set
                  by (smt add_lessD1 leI n_prop nth_default_def sorted_nth_mono sorted_root_list_set_def)
                have "r < ?elt2" using r_prop by auto
                then have ilt: " i < n + 1" using i_prop sorted_sorted_list_of_set
                  by (smt leI n_prop nth_default_def sorted_nth_mono sorted_root_list_set_def) 
                then show "False"  using igt ilt
                  by auto
              qed
              then show ?thesis by auto
            qed
            then have nor: "¬(r. d * r^2 + e * r + f = 0  r > ?elt r  x)"
              using xltel2 xgtel by auto
            then have xltz: "d*x^2 + e*x + f < 0" using inset x_prop by auto
            show "d * q2 + e * q + f < 0"
              using qlt qgt nor changes_sign_var[of d _ e f _] xltz unfolding sign_num_def
              by smt 
          qed
          then have " ((d, e, f)set les. y'>?elt. x{?elt<..y'}. d * x2 + e * x + f < 0)"
            using xgtel xltel2 by auto
          then have "((a, b, c)set les. a*?elt^2 + b*?elt + c = 0 
                ((d, e, f)set les. y'>?elt. x{?elt<..y'}. d * x2 + e * x + f < 0))"
            using exabc by auto
          then show "(k. (a, b, c)set les. a*k^2 + b*k + c = 0 
                ((d, e, f)set les. y'>k. x{k<..y'}. d * x2 + e * x + f < 0))"
            by auto
        qed
        then have inbetw: "(n. (n+1) < (length ?srl)  x > nth_default 0 ?srl n  x < nth_default 0 ?srl (n + 1))  False"
          using nok by auto
        have lenzer: "length xa = 0  False" 
        proof - 
          assume "length xa = 0"
          have xis: "x > w  x < w"
            using notmem Cons.hyps
            by (smt list.set_intros(1) same_set xnotin) 
          have xgt: "x > w  False"
          proof - 
            assume xgt: "x > w"
            show "False" using posinf Cons.hyps
              by (metis One_nat_def Suc_eq_plus1 ‹length xa = 0 cancel_comm_monoid_add_class.diff_cancel list.size(4) nth_default_Cons_0 xgt)
          qed
          have xlt: "x < w  False"
          proof - 
            assume xlt: "x < w"
            show "False" using neginf Cons.hyps
              by (metis nth_default_Cons_0 xlt) 
          qed
          show "False" using xis xgt xlt by auto
        qed
        have lengt: "length xa > 0  False"
        proof - 
          assume "length xa > 0"
          have "x  nth_default 0 ?srl 0" using neginf
            by fastforce
          then have xgtf: "x > nth_default 0 ?srl 0" using notmem
            using Cons.hyps(2) by fastforce
          have "x  nth_default 0 ?srl (length ?srl - 1)" using posinf by fastforce
          then have "(n. (n+1) < (length ?srl)  x  nth_default 0 ?srl n  x  nth_default 0 ?srl (n + 1))"
            using lengthsrl xgtf notmem sorted_list_prop[where l = ?srl, where x = "x"]
            by (metis add_lessD1 diff_less nth_default_nth sorted_root_list_set_def sorted_sorted_list_of_set zero_less_one)
          then obtain n where n_prop: "(n+1) < (length ?srl)  x  nth_default 0 ?srl n  x  nth_default 0 ?srl (n + 1)" by auto
          then have "x > nth_default 0 ?srl n  x < nth_default 0 ?srl (n+1)"
            using notmem
            by (metis Suc_eq_plus1 Suc_lessD less_eq_real_def)
          then have "(n. (n+1) < (length ?srl)  x > nth_default 0 ?srl n  x < nth_default 0 ?srl (n + 1))"
            using n_prop
            by blast  
          then show "False" using inbetw by auto
        qed
        then show ?case using lenzer lengt by auto
      qed 
    qed
    show "False"
      using h1 h2 by auto
  qed
  then have equiv_false: "¬(((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  
               ((a', b', c')set les.
               a' = 0 
               b'  0  ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0)) 
        
        ((a', b', c')set les.
               a'  0 
               4 * a' * c'  b'2 
               ((d, e, f)set les.
                   y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                      x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)) 
      
      ((a', b', c')set les.  a'  0 
               4 * a' * c'  b'2 
                ((d, e, f)set les.
                    y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                       x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                          d * x2 + e * x + f < 0)))  False"
    by linarith
  have "¬(((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))  False"
  proof - 
    assume "¬(((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))"
    then have "¬(((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0)  
               ((a', b', c')set les.
               a' = 0 
               b'  0  ((d, e, f)set les. y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0)) 
        
        ((a', b', c')set les.
               a'  0 
               4 * a' * c'  b'2 
               ((d, e, f)set les.
                   y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                      x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}. d * x2 + e * x + f < 0)) 
      
      ((a', b', c')set les.  a'  0 
               4 * a' * c'  b'2 
                ((d, e, f)set les.
                    y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                       x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                          d * x2 + e * x + f < 0)))"
      by auto
    then show ?thesis
      using equiv_false by auto
  qed
  then show ?thesis
    by blast 
qed

lemma les_qe : 
  shows "(x. ((a, b, c)set les. a * x2 + b * x + c < 0)) =
    (((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))"
proof -
  have first: "(x. ((a, b, c)set les. a * x2 + b * x + c < 0)) 
    (((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))"
    using les_qe_backward by auto
  have second: "(((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))  (x. ((a, b, c)set les. a * x2 + b * x + c < 0)) "
    using les_qe_forward by auto
  have "(x. ((a, b, c)set les. a * x2 + b * x + c < 0)) 
  (((a, b, c)set les. x. y<x. a * y2 + b * y + c < 0) 
     ((a', b', c')set les.
         a' = 0 
         b'  0 
         ((d, e, f)set les.
             y'>- (c' / b'). x{- (c' / b')<..y'}. d * x2 + e * x + f < 0) 
         a'  0 
         4 * a' * c'  b'2 
         (((d, e, f)set les.
              y'>(sqrt (b'2 - 4 * a' * c') - b') / (2 * a').
                 x{(sqrt (b'2 - 4 * a' * c') - b') / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0) 
          ((d, e, f)set les.
              y'>(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a').
                 x{(- b' - sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
                    d * x2 + e * x + f < 0))))"
    using first second
    by meson 
  then show ?thesis
    by blast
qed


subsubsection "equiv\\_lemma"
lemma equiv_lemma: 
  assumes big_asm: "((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0)) 
  ((a', b', c')set eq.
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
          
      ((a', b', c')set eq. a'  0 
         - b'2 + 4 * a' * c'  0  ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0)) 
     (((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))"
  shows "(((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0) 
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0) 
          ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
     ((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))" 
proof - 
  let ?t = " (((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0) 
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0) 
          ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
     ((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))"
  have h1: "((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0))  ?t"
    by auto
  have h2: "((a', b', c')set eq.
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0)))  ?t" 
    by auto
  have h3: "((a', b', c')set eq. a'  0 
         - b'2 + 4 * a' * c'  0  ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))  ?t" 
    by auto
  show ?thesis
    using big_asm h1 h2 h3
    by presburger 
qed

subsubsection "The eq\\_qe lemma"
lemma eq_qe_forwards: 
  shows "(x. ((a, b, c)set eq. a * x2 + b * x + c = 0) 
         ((a, b, c)set les. a * x2 + b * x + c < 0))  
    (((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0) 
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0) 
          ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
     ((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))"
proof - 
  let ?big_or = "((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0)) 
  ((a', b', c')set eq.
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
          
      ((a', b', c')set eq. a'  0 
         - b'2 + 4 * a' * c'  0  ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0)) 
     (((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))"
  assume asm: "(x. ((a, b, c)set eq. a * x2 + b * x + c = 0) 
         ((a, b, c)set les. a * x2 + b * x + c < 0)) " 
  then obtain x where x_prop: "((a, b, c)set eq. a * x2 + b * x + c = 0) 
         ((a, b, c)set les. a * x2 + b * x + c < 0)" by auto
  have "¬ ((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0)) 
  ¬ ((a', b', c')set eq.
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
          ¬ ((a', b', c')set eq. a'  0 
         - b'2 + 4 * a' * c'  0  ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0)) 
     ¬ (((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))  False" 
  proof - 
    assume big_conj: "¬ ((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0)) 
  ¬ ((a', b', c')set eq.
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0))) 
          ¬ ((a', b', c')set eq. a'  0 
         - b'2 + 4 * a' * c'  0  ((d, e, f)set eq.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0)) 
     ¬ (((d, e, f)set eq. d = 0  e = 0  f = 0) 
     (x. (a, b, c)set les. a * x2 + b * x + c < 0))"
    have not_lin: "¬((a', b', c')set eq.
         (a' = 0  b'  0) 
         ((d, e, f)set eq. d * (- c' / b')2 + e * (- c' / b') + f = 0) 
         ((d, e, f)set les. d * (- c' / b')2 + e * (- c' / b') + f < 0))"
      using big_conj by auto
    have not_quad1: "¬((a', b', c')set eq.
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set eq.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f =
              0) 
          ((d, e, f)set les.
              d * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a'))2 +
              e * ((- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')) +
              f
              < 0)))"
      using big_conj by auto
    have not_quad2: "¬(