# Theory QE

section "QE lemmas"
theory QE
imports Polynomials.MPoly_Type_Univariate
Polynomials.Polynomials  Polynomials.MPoly_Type_Class_FMap

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: "¬(