# 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

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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + b * x + c = 0 ⟷ x = -r"
proof -
have "c = a*r^2" using root
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"
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 * x⇧2 + b * x + c = 0 ⟷ x = -b / (2 * a)"
using discriminant_zero aneq unfolding discrim_def by auto
then show ?thesis using beq
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 "∃c∈root_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 * x⇧2 + b * x + c) ≠ sign_num (a * y⇧2 + 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 * q⇧2 + 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 * x⇧2 + b * x + c = 0 ⟹ (a = 0 ∧ b = 0 ∧ c = 0)"
proof -
assume r_lt: "r < p"
assume inf_zer: "∀x∈{r <..p}. a * x⇧2 + 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"

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)"
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)"
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))"
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

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

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 * x⇧2 + e * x + f < 0) ⟹
(∃y'>q. (∀(d, e, f)∈set les. ∀x∈{q<..y'}. d * x⇧2 + e * x + f < 0))"
proof (induct les)
case Nil
then show ?case using gt_ex by auto
next
case (Cons z les)
have "∀a∈set les. case a of (d, e, f) ⇒ ∃y'>q. ∀x∈{q<..y'}. d * x⇧2 + e * x + f < 0"
using  Cons.prems by auto
then have " ∃y'>q. ∀a∈set les. case a of (d, e, f) ⇒ ∀x∈{q<..y'}. d * x⇧2 + e * x + f < 0"
using Cons.hyps by auto
then obtain y1 where y1_prop : "y1>q ∧ (∀a∈set les. case a of (d, e, f) ⇒ ∀x∈{q<..y1}. d * x⇧2 + e * x + f < 0)"
by auto
have "case z of (d, e, f) ⇒ ∃y'>q. ∀x∈{q<..y'}. d * x⇧2 + 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 * x⇧2 + e * x + f < 0))"
by auto
let ?y = "min y1 y2"
have "?y > q ∧ (∀a∈set (z#les). case a of (d, e, f) ⇒ ∀x∈{q<..?y}. d * x⇧2 + 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 * x⇧2 + e * x + f < 0)"
shows "(∃x. (∀(a, b, c)∈set les. a * x⇧2 + b * x + c < 0))"
proof -
have "(∀(d, e, f)∈set les. ∃y'>r. ∀x∈{r<..y'}. d * x⇧2 + e * x + f < 0) ⟹
(∃y'>r. (∀(d, e, f)∈set les. ∀x∈{r<..y'}. d * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 2 * a * r*x + c < 0"
proof -
fix y'
assume beq: "b = 2 * a * r"
assume aprop: " ¬ a < 0"
assume root: " a * r⇧2 - 2 * a *r*r + c = 0"
assume rootlt: "- r < y'"
show " ∃x∈{- r<..y'}. ¬ a * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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)"
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 * x⇧2 + 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:]"]
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:]"]
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 * x⇧2 + e * x + f ≤ 0) ⟹
(∃y'>q. (∀(d, e, f)∈set leq. ∀x∈{q<..y'}. d * x⇧2 + e * x + f ≤ 0))"
proof (induct leq)
case Nil
then show ?case using gt_ex by auto
next
case (Cons z leq)
have "∀a∈set leq. case a of (d, e, f) ⇒ ∃y'>q. ∀x∈{q<..y'}. d * x⇧2 + e * x + f ≤ 0"
using  Cons.prems by auto
then have " ∃y'>q. ∀a∈set leq. case a of (d, e, f) ⇒ ∀x∈{q<..y'}. d * x⇧2 + e * x + f ≤ 0"
using Cons.hyps by auto
then obtain y1 where y1_prop : "y1>q ∧ (∀a∈set leq. case a of (d, e, f) ⇒ ∀x∈{q<..y1}. d * x⇧2 + e * x + f ≤ 0)"
by auto
have "case z of (d, e, f) ⇒ ∃y'>q. ∀x∈{q<..y'}. d * x⇧2 + 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 * x⇧2 + e * x + f ≤ 0))"
by auto
let ?y = "min y1 y2"
have "?y > q ∧ (∀a∈set (z#leq). case a of (d, e, f) ⇒ ∀x∈{q<..?y}. d * x⇧2 + 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 * x⇧2 + e * x + f ≠ 0) ⟹
(∃y'>q. (∀(d, e, f)∈set neq. ∀x∈{q<..y'}. d * x⇧2 + e * x + f ≠ 0))"
proof (induct neq)
case Nil
then show ?case using gt_ex by auto
next
case (Cons z neq)
have "∀a∈set neq. case a of (d, e, f) ⇒ ∃y'>q. ∀x∈{q<..y'}. d * x⇧2 + e * x + f ≠ 0"
using  Cons.prems by auto
then have " ∃y'>q. ∀a∈set neq. case a of (d, e, f) ⇒ ∀x∈{q<..y'}. d * x⇧2 + e * x + f ≠ 0"
using Cons.hyps by auto
then obtain y1 where y1_prop : "y1>q ∧ (∀a∈set neq. case a of (d, e, f) ⇒ ∀x∈{q<..y1}. d * x⇧2 + e * x + f ≠ 0)"
by auto
have "case z of (d, e, f) ⇒ ∃y'>q. ∀x∈{q<..y'}. d * x⇧2 + 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 * x⇧2 + e * x + f ≠ 0))"
by auto
let ?y = "min y1 y2"
have "?y > q ∧ (∀a∈set (z#neq). case a of (d, e, f) ⇒ ∀x∈{q<..?y}. d * x⇧2 + e * x + f ≠ 0)"
using y1_prop y2_prop
by force
then show ?case
by blast
qed

subsection "Some Casework"

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 ≤ b⇧2 - 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
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"
have h1: "(a*b^2)/(4*a^2) = (b^2)/(4*a)"
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)"
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"]
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

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)"
then have "∃k > y.  a*k^2 + b*k + c > 0"
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:]"]
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

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

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 * x⇧2 + 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 * x⇧2 + 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
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
by (metis greaterThanAtMost_iff)
qed
have aneq: "a ≠ 0 ⟹∃y'>- r. ∀x∈{-r<..y'}. a * x⇧2 + b * x + c < 0"
proof -
assume aneq: "(a::real) ≠ 0"
have "b^2 - 4*a*c < 0 ⟹ a * r⇧2 + b * r + c ≠ 0" using root discriminant_negative[of a b c r] unfolding discrim_def
using aneq by auto
then have " a * r⇧2 + b * r + c ≠ 0 ⟹
a * r⇧2 - b * r + c = 0 ⟹
b⇧2 < 4 * a * c ⟹ False"
proof -
assume a1: "a * r⇧2 - b * r + c = 0"
assume a2: "b⇧2 < 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 * r⇧2 + - 1 * b * r = a * r⇧2 + c + - 1 * b * r"
by auto
have f6: "∀x0 x1 x2 x3. (x3::real) * x0⇧2 + x2 * x0 + x1 = x1 + x3 * x0⇧2 + 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 = ra⇧2 + - 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 * r⇧2 + 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 ‹b⇧2 - 4 * a * c < 0 ⟹ a * r⇧2 + b * r + c ≠ 0› by auto
then have discrim: "b⇧2 ≥ 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 * x⇧2 + b * x + c = 0 ∧ a * y⇧2 + 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 * x⇧2 + b * x + c = 0 ∧ a * y⇧2 + 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 (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)› 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 (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)› 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 * x⇧2 + 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 (b⇧2 - c * (4 * a)) < - b + sqrt (b⇧2 - c * (4 * a))"
by (metis ‹- b - sqrt (b⇧2 - 4 * a * c) < - b + sqrt (b⇧2 - 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 (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)› 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 * x⇧2 + 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 (b⇧2 - 4 * a * c)) / (2 * a)› greaterThanAtMost_iff xy_prop by auto
then show "∃y'>- r. ∀x∈{-r<..y'}. a * x⇧2 + b * x + c < 0"
using k_prop using ‹x = - r ∧ y = (- b + sqrt (b⇧2 - 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 * x⇧2 + 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 * x⇧2 + 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<```