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 greaterThanAtMost_iff less_add_one less_eq_real_def linorder_not_le no_zer poly_IVT_pos r_ltz)
  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, opaque_lifting) Polynomial.poly_minus minus_pCons mult_minus1 neg_equal_0_iff_equal)
  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, opaque_lifting) minus_less_iff minus_mult_commute mult_1 power2_eq_iff)
  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 discrim_def 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
  h