Theory Quadratic

(* ----------------------------------------------------------------- *)
subsection ‹Quadratic equations›
(* ----------------------------------------------------------------- *)

text ‹In this section some simple properties of quadratic equations and their roots are derived.
Quadratic equations over reals and over complex numbers, but also systems of quadratic equations and
systems of quadratic and linear equations are analysed.›

theory Quadratic
  imports More_Complex "HOL-Library.Quadratic_Discriminant"
begin

(* ----------------------------------------------------------------- *)
subsubsection ‹Real quadratic equations, Viette rules›
(* ----------------------------------------------------------------- *)

lemma viette2_monic:
  fixes b c ξ1 ξ2 :: real
  assumes "b2 - 4*c  0" and "ξ12 + b*ξ1 + c = 0" and "ξ22 + b*ξ2 + c = 0" and "ξ1  ξ2"
  shows "ξ1*ξ2 = c"
  using assms
  by algebra

lemma viette2:
  fixes a b c ξ1 ξ2 :: real
  assumes "a  0" and "b2 - 4*a*c  0" and "a*ξ12 + b*ξ1 + c = 0" and "a*ξ22 + b*ξ2 + c = 0" and "ξ1  ξ2"
  shows "ξ1*ξ2 = c/a"
proof (rule viette2_monic[of "b/a" "c/a" ξ1 ξ2])
  have "(b / a)2 - 4 * (c / a) = (b2 - 4*a*c) / a2"
    using a  0
    by (auto simp add: power2_eq_square field_simps)
  thus "0  (b / a)2 - 4 * (c / a)"
    using b2 - 4*a*c  0
    by simp
next
  show "ξ12 + b / a * ξ1 + c / a = 0" "ξ22 + b / a * ξ2 + c / a = 0"
    using assms
    by (auto simp add: power2_eq_square field_simps)
next
  show "ξ1  ξ2"
    by fact
qed

lemma viette2'_monic:
  fixes b c ξ :: real
  assumes "b2 - 4*c = 0" and "ξ2 + b*ξ + c = 0"
  shows "ξ*ξ = c"
  using assms
  by algebra

lemma viette2':
  fixes a b c ξ :: real
  assumes "a  0" and "b2 - 4*a*c = 0" and "a*ξ2 + b*ξ + c = 0"
  shows "ξ*ξ = c/a"
proof (rule viette2'_monic)
  have "(b / a)2 - 4 * (c / a) = (b2 - 4*a*c) / a2"
    using a  0
    by (auto simp add: power2_eq_square field_simps)
  thus "(b / a)2 - 4 * (c / a) = 0"
    using b2 - 4*a*c = 0
    by simp
next
  show "ξ2 + b / a * ξ + c / a = 0"
    using assms
    by (auto simp add: power2_eq_square field_simps)
qed

(* ----------------------------------------------------------------- *)
subsubsection ‹Complex quadratic equations›
(* ----------------------------------------------------------------- *)

lemma complex_quadratic_equation_monic_only_two_roots:
  fixes ξ :: complex
  assumes "ξ2 + b * ξ + c = 0"
  shows "ξ = (-b + ccsqrt(b2 - 4*c)) / 2  ξ = (-b - ccsqrt(b2 - 4*c)) / 2"
using assms
proof-
  from assms have "(2 * (ξ + b/2))2 = b2 - 4*c"
    by (simp add: power2_eq_square field_simps)
       (metis (no_types, lifting) distrib_right_numeral mult.assoc mult_zero_left)
  hence "2 * (ξ + b/2) = ccsqrt (b2 - 4*c)  2 * (ξ + b/2) = - ccsqrt (b2 - 4*c)"
    using ccsqrt[of "(2 * (ξ + b / 2))" "b2 - 4 * c"]
    by (simp add: power2_eq_square)
  thus ?thesis
    using mult_cancel_right[of "b + ξ * 2" 2 "ccsqrt (b2 - 4*c)"]
    using mult_cancel_right[of "b + ξ * 2" 2 "-ccsqrt (b2 - 4*c)"]
    by (auto simp add: field_simps) (metis add_diff_cancel diff_minus_eq_add minus_diff_eq)
qed

lemma complex_quadratic_equation_monic_roots:
  fixes ξ :: complex
  assumes "ξ = (-b + ccsqrt(b2 - 4*c)) / 2 
           ξ = (-b - ccsqrt(b2 - 4*c)) / 2"
  shows  "ξ2 + b * ξ + c = 0"
using assms
proof
  assume *: "ξ = (- b + ccsqrt (b2 - 4 * c)) / 2"
  show ?thesis
    by ((subst *)+) (subst power_divide, subst power2_sum, simp add: field_simps, simp add: power2_eq_square)
next
  assume *: "ξ = (- b - ccsqrt (b2 - 4 * c)) / 2"
  show ?thesis
    by ((subst *)+, subst power_divide, subst power2_diff, simp add: field_simps, simp add: power2_eq_square)
qed

lemma complex_quadratic_equation_monic_distinct_roots:
  fixes b c :: complex
  assumes "b2 - 4*c  0"
  shows " k1 k2. k1  k2  k12 + b*k1 + c = 0  k22 + b*k2 + c = 0"
proof-
  let ?ξ1 = "(-b + ccsqrt(b2 - 4*c)) / 2"
  let ?ξ2 = "(-b - ccsqrt(b2 - 4*c)) / 2"
  show ?thesis
    apply (rule_tac x="?ξ1" in exI)
    apply (rule_tac x="?ξ2" in exI)
    using assms 
    using complex_quadratic_equation_monic_roots[of ?ξ1 b c]
    using complex_quadratic_equation_monic_roots[of ?ξ2 b c]
    by simp
qed

lemma complex_quadratic_equation_two_roots:
  fixes ξ :: complex
  assumes "a  0" and "a*ξ2 + b * ξ + c = 0"
  shows "ξ = (-b + ccsqrt(b2 - 4*a*c)) / (2*a) 
         ξ = (-b - ccsqrt(b2 - 4*a*c)) / (2*a)"
proof-
  from assms have "ξ2 + (b/a) * ξ + (c/a) = 0"
    by (simp add: field_simps)
  hence "ξ = (-(b/a) + ccsqrt((b/a)2 - 4*(c/a))) / 2  ξ = (-(b/a) - ccsqrt((b/a)2 - 4*(c/a))) / 2"
    using complex_quadratic_equation_monic_only_two_roots[of ξ "b/a" "c/a"]
    by simp
  hence " k. ξ = (-(b/a) + (-1)^k * ccsqrt((b/a)2 - 4*(c/a))) / 2"
    by safe (rule_tac x="2" in exI, simp, rule_tac x="1" in exI, simp)
  then obtain k1 where "ξ = (-(b/a) + (-1)^k1 * ccsqrt((b/a)2 - 4*(c/a))) / 2"
    by auto
  moreover
  have "(b / a)2 - 4 * (c / a) = (b2 - 4 * a * c) * (1 / a2)"
    using a  0
    by (simp add: field_simps power2_eq_square)
  hence "ccsqrt ((b / a)2 - 4 * (c / a)) = ccsqrt (b2 - 4 * a * c) * ccsqrt (1/a2) 
         ccsqrt ((b / a)2 - 4 * (c / a)) = - ccsqrt (b2 - 4 * a * c) * ccsqrt (1/a2)"
    using ccsqrt_mult[of "b2 - 4 * a * c" "1/a2"]
    by auto
  hence " k.  ccsqrt ((b / a)2 - 4 * (c / a)) = (-1)^k * ccsqrt (b2 - 4 * a * c) * ccsqrt (1 / a2)"
    by safe (rule_tac x="2" in exI, simp, rule_tac x="1" in exI, simp)
  then obtain k2 where "ccsqrt ((b / a)2 - 4 * (c / a)) = (-1)^k2 * ccsqrt (b2 - 4 * a * c) * ccsqrt (1 / a2)"
    by auto
  moreover
  have "ccsqrt (1 / a2) = 1/a  ccsqrt (1 / a2) = -1/a"
    using ccsqrt[of "1/a" "1 / a2"]
    by (auto simp add: power2_eq_square)
  hence " k. ccsqrt (1 / a2) = (-1)^k * 1/a"
    by safe (rule_tac x="2" in exI, simp, rule_tac x="1" in exI, simp)
  then obtain k3 where "ccsqrt (1 / a2) = (-1)^k3 * 1/a"
    by auto
  ultimately
  have "ξ = (- (b / a) + ((-1) ^ k1 * (-1) ^ k2 * (-1) ^ k3) * ccsqrt (b2 - 4 * a * c) * 1/a) / 2"
    by simp
  moreover
  have "(-(1::complex)) ^ k1 * (-1) ^ k2 * (-1) ^ k3 = 1  (-(1::complex)) ^ k1 * (-1) ^ k2 * (-1) ^ k3 = -1"
    using neg_one_even_power[of "k1 + k2 + k3"]
    using neg_one_odd_power[of "k1 + k2 + k3"]
    by (smt power_add)
  ultimately
  have "ξ = (- (b / a) + ccsqrt (b2 - 4 * a * c) * 1 / a) / 2  ξ = (- (b / a) - ccsqrt (b2 - 4 * a * c) * 1 / a) / 2"
    by auto
  thus ?thesis
    using a  0
    by (simp add: field_simps)
qed

lemma complex_quadratic_equation_only_two_roots:
  fixes x :: complex
  assumes "a  0"
  assumes "qf = (λ x. a*x2 + b*x + c)"
          "qf x1 = 0" and "qf x2 = 0" and "x1  x2"
          "qf x = 0"
  shows "x = x1  x = x2"
  using assms
  using complex_quadratic_equation_two_roots
  by blast


(* ----------------------------------------------------------------- *)
subsubsection ‹Intersections of linear and quadratic forms›
(* ----------------------------------------------------------------- *)
(* These lemmas are not used *)

lemma quadratic_linear_at_most_2_intersections_help:
  fixes x y :: complex
  assumes "(a11, a12, a22)  (0, 0, 0)" and "k2  0"
          "qf = (λ x y. a11*x2 + 2*a12*x*y + a22*y2 + b1*x + b2*y + c)" and "lf = (λ x y. k1*x + k2*y + n)"
          "qf x y = 0" and "lf x y = 0"
          "pf = (λ x. (a11 - 2*a12*k1/k2 + a22*k12/k22)*x2 + (-2*a12*n/k2  + b1 + a22*2*n*k1/k22 - b2*k1/k2)*x + a22*n2/k22 - b2*n/k2 + c)"
          "yf = (λ x. (-n - k1*x) / k2)"
  shows "pf x = 0" and "y = yf x"
proof -
  show "y = yf x"
    using assms
    by (simp add:field_simps eq_neg_iff_add_eq_0)
next
  have "2*a12*x*(-n - k1*x)/k2 = (-2*a12*n/k2)*x - (2*a12*k1/k2)*x2"
    by algebra
  have "a22*((-n - k1*x)/k2)2 = a22*n2/k22 + (a22*2*n*k1/k22)*x + (a22*k12/k22)*x2"
    by (simp add: power_divide) algebra
  have "2*a12*x*(-n - k1*x)/k2 = (-2*a12*n/k2)*x - (2*a12*k1/k2)*x2"
    by algebra
  have "b2*(-n - k1*x)/k2 = -b2*n/k2 - (b2*k1/k2)*x"
    by algebra

  have *: "y = (-n - k1*x)/k2"
    using assms(2, 4, 6)
    by (simp add:field_simps eq_neg_iff_add_eq_0)

  have "0 = a11*x2 + 2*a12*x*y + a22*y2 + b1*x + b2*y + c"
    using assms
    by simp
  hence "0 = a11*x2 + 2*a12*x*(-n - k1*x)/k2 + a22*((-n - k1*x)/k2)2 + b1*x + b2*(-n - k1*x)/k2 + c"
    by (subst (asm) *, subst (asm) *, subst (asm) *) auto
  also have "... = (a11 - 2*a12*k1/k2 + a22*k12/k22)*x2 + (-2*a12*n/k2  + b1 + a22*2*n*k1/k22 - b2*k1/k2)*x + a22*n2/k22 -b2*n/k2 + c"
    using 2*a12*x*(-n - k1*x)/k2 = (-2*a12*n/k2)*x - (2*a12*k1/k2)*x2
    using a22*((-n - k1*x)/k2)2 = a22*n2/k22 + (a22*2*n*k1/k22)*x + (a22*k12/k22)*x2
    using b2*(-n - k1*x)/k2 = -b2*n/k2 - (b2*k1/k2)*x
    by (simp add:field_simps)
  finally show "pf x = 0"
    using assms(7)
    by auto
qed

lemma quadratic_linear_at_most_2_intersections_help':
  fixes x y :: complex
  assumes "qf = (λ x y. a11*x2 + 2*a12*x*y + a22*y2 + b1*x + b2*y + c)"
          "x = -n/k1" and "k1  0" and "qf x y = 0"
          "yf = (λ y. k12*a22*y2 + (-2*a12*n*k1 + b2*k12)*y + a11*n2 - b1*n*k1 + c*k12)"
  shows "yf y = 0"
proof-
  have "0 = a11*n2/k12 - 2*a12*n*y/k1 + a22*y2 - b1*n/k1 + b2*y + c"
    using assms(1, 2, 4)
    by (simp add: power_divide)
  hence "0 = a11*n2 - 2*a12*n*k1*y + a22*y2*k12 - b1*n*k1 + b2*y*k12 + c*k12"
    using assms(3)
    apply (simp add:field_simps power2_eq_square)
    by algebra
  thus ?thesis
    using assms(1, 4, 5)
    by (simp add:field_simps)
qed

lemma quadratic_linear_at_most_2_intersections:
  fixes x y x1 y1 x2 y2 :: complex
  assumes "(a11, a12, a22)  (0, 0, 0)" and "(k1, k2)  (0, 0)"
  assumes "a11*k22 - 2*a12*k1*k2 + a22*k12  0"
  assumes "qf = (λ x y. a11*x2 + 2*a12*x*y + a22*y2 + b1*x + b2*y + c)" and "lf = (λ x y. k1*x + k2*y + n)"
          "qf x1 y1 = 0" and "lf x1 y1 = 0"
          "qf x2 y2 = 0" and "lf x2 y2 = 0"
          "(x1, y1)  (x2, y2)"
          "qf x y = 0" and "lf x y = 0"
  shows "(x, y) = (x1, y1)  (x, y) = (x2, y2)"
proof(cases "k2 = 0")
  case True
  hence "k1  0"
    using assms(2)
    by simp

  have "a22*k12  0"
    using assms(3) True
    by auto

  have "x1 = -n/k1"
    using k1  0 assms(5, 7) True
    by (metis add.right_neutral add_eq_0_iff2 mult_zero_left nonzero_mult_div_cancel_left)
  have "x2 = -n/k1"
    using k1  0 assms(5, 9) True
    by (metis add.right_neutral add_eq_0_iff2 mult_zero_left nonzero_mult_div_cancel_left)
  have "x = -n/k1"
    using k1  0 assms(5, 12) True
    by (metis add.right_neutral add_eq_0_iff2 mult_zero_left nonzero_mult_div_cancel_left)

  let ?yf =  "(λ y. k12*a22*y2 + (-2*a12*n*k1 + b2*k12)*y + a11*n2 - b1*n*k1 + c*k12)"

  have "?yf y = 0"
    using quadratic_linear_at_most_2_intersections_help'[of qf a11 a12 a22 b1 b2 c x n k1 y ?yf]
    using assms(4, 11) k1  0 x = -n/k1
    by auto
  have "?yf y1 = 0"
    using quadratic_linear_at_most_2_intersections_help'[of qf a11 a12 a22 b1 b2 c x1 n k1 y1 ?yf]
    using assms(4, 6) k1  0 x1 = -n/k1
    by auto
  have "?yf y2 = 0"
    using quadratic_linear_at_most_2_intersections_help'[of qf a11 a12 a22 b1 b2 c x2 n k1 y2 ?yf]
    using assms(4, 8) k1  0 x2 = -n/k1
    by auto

  have "y1  y2"
    using assms(10) x1 = -n/k1 x2 = -n/k1
    by blast

  have "y = y1  y = y2"
    using complex_quadratic_equation_only_two_roots[of "a22*k12" ?yf "-2*a12*n*k1 + b2*k12" "a11*n2 - b1*n*k1 + c*k12"
                                                        y1 y2 y]
    using a22*k12  0 ?yf y1 = 0 y1  y2 ?yf y2 = 0 ?yf y = 0
    by fastforce

  thus ?thesis
    using x1 = -n/k1 x2 = -n/k1  x = -n/k1
    by auto
next
  case False

  let ?py = "(λ x. (-n - k1*x)/k2)"
  let ?pf = "(λ x. (a11 - 2*a12*k1/k2 + a22*k12/k22)*x2 + (-2*a12*n/k2  + b1 + a22*2*n*k1/k22 - b2*k1/k2)*x + a22*n2/k22 -b2*n/k2 + c)"
  have "?pf x1 = 0" "y1 = ?py x1"
    using quadratic_linear_at_most_2_intersections_help[of a11 a12 a22 k2 qf b1 b2 c lf k1 n x1 y1]
    using assms(1, 4, 5, 6, 7) False
    by auto
  have "?pf x2 = 0" "y2 = ?py x2"
    using quadratic_linear_at_most_2_intersections_help[of a11 a12 a22 k2 qf b1 b2 c lf k1 n x2 y2]
    using assms(1, 4, 5, 8, 9) False
    by auto
  have "?pf x = 0" "y = ?py x"
    using quadratic_linear_at_most_2_intersections_help[of a11 a12 a22 k2 qf b1 b2 c lf k1 n x y]
    using assms(1, 4, 5, 11, 12) False
    by auto

  have "x1  x2"
    using assms(10) y1 = ?py x1 y2 = ?py x2
    by auto

  have "a11 - 2*a12*k1/k2 + a22*k12/k22 = (a11 * k22 - 2 * a12 * k1 * k2 + a22 * k12)/k22"
    by (simp add: False power2_eq_square add_divide_distrib diff_divide_distrib)
  also have "...   0"
    using False assms(3)
    by simp
  finally have "a11 - 2*a12*k1/k2 + a22*k12/k22  0"
    .

  have "x = x1  x = x2"
    using complex_quadratic_equation_only_two_roots[of "a11 - 2*a12*k1/k2 + a22*k12/k22" ?pf
                                                       "(- 2 * a12 * n / k2 + b1 + a22 * 2 * n * k1 / k22 - b2 * k1 / k2)"
                                                       "a22 * n2 / k22 - b2 * n / k2 + c" x1 x2 x]
    using ?pf x2 = 0 ?pf x1 = 0 ?pf x = 0
    using a11 - 2 * a12 * k1 / k2 + a22 * k12 / k22  0
    using x1  x2
    by fastforce

  thus ?thesis
    using y = ?py x y1 = ?py x1 y2 = ?py x2
    by (cases "x = x1", auto)
qed

lemma quadratic_quadratic_at_most_2_intersections':
  fixes x y x1 y1 x2 y2 :: complex
  assumes "b2  B2  b1  B1"
          "(b2 - B2)2 + (b1 - B1)2  0"
  assumes "qf1 = (λ x y. x2 + y2 + b1*x + b2*y + c)"
          "qf2 = (λ x y. x2 + y2 + B1*x + B2*y + C)"
          "qf1 x1 y1 = 0" "qf2 x1 y1 = 0"
          "qf1 x2 y2 = 0" "qf2 x2 y2 = 0"
          "(x1, y1)  (x2, y2)"
          "qf1 x y = 0" "qf2 x y = 0"
  shows "(x, y) = (x1, y1)  (x, y) = (x2, y2)"
proof-
  have "x2 + y2 + b1*x + b2*y + c = 0"
    using assms by auto
  have "x2 + y2 + B1*x + B2*y + C = 0"
    using assms by auto
  hence "0 = x2 + y2 + b1*x + b2*y + c - (x2 + y2 + B1*x + B2*y + C)"
    using x2 + y2 + b1*x + b2*y + c = 0
    by auto
  hence "0 = (b1 - B1)*x + (b2 - B2)*y + c - C"
    by (simp  add:field_simps) 
  
  have "x12 + y12 + b1*x1 + b2*y1 + c = 0"
    using assms  by auto
  have "x12 + y12 + B1*x1 + B2*y1 + C = 0"
    using assms by auto
  hence "0 = x12 + y12 + b1*x1 + b2*y1 + c - (x12 + y12 + B1*x1 + B2*y1 + C)"
    using x12 + y12 + b1*x1 + b2*y1 + c = 0
    by auto
  hence "0 = (b1 - B1)*x1 + (b2 - B2)*y1 + c - C"
    by (simp  add:field_simps) 

  have "x22 + y22 + b1*x2 + b2*y2 + c = 0"
    using assms  by auto
  have "x22 + y22 + B1*x2 + B2*y2 + C = 0"
    using assms  by auto
  hence "0 = x22 + y22 + b1*x2 + b2*y2 + c - (x22 + y22 + B1*x2 + B2*y2 + C)"
    using x22 + y22 + b1*x2 + b2*y2 + c = 0
    by auto
  hence "0 = (b1 - B1)*x2 + (b2 - B2)*y2 + c - C"
    by (simp  add:field_simps)  

  have "(b1 - B1, b2 - B2)  (0, 0)"
    using assms(1) by auto

  let ?lf = "(λ x y. (b1 - B1)*x + (b2 - B2)*y + c - C)"

  have "?lf x y = 0" "?lf x1 y1 = 0" "?lf x2 y2 = 0"
    using 0 = (b1 - B1)*x2 + (b2 - B2)*y2 + c - C
          0 = (b1 - B1)*x1 + (b2 - B2)*y1 + c - C
          0 = (b1 - B1)*x + (b2 - B2)*y + c - C
    by auto

  thus ?thesis
    using quadratic_linear_at_most_2_intersections[of 1 0 1 "b1 - B1" "b2 - B2" qf1 b1 b2 c ?lf "c - C" x1 y1 x2 y2 x y]
    using (b1 - B1, b2 - B2)  (0, 0)
    using assms (b1 - B1, b2 - B2)  (0, 0)
    using (b1 - B1) * x + (b2 - B2) * y + c - C = 0 (b1 - B1) * x1 + (b2 - B2) * y1 + c - C = 0
    by (simp add: add_diff_eq)
qed

lemma quadratic_change_coefficients:
  fixes x y :: complex
  assumes "A1  0" 
  assumes "qf = (λ x y. A1*x2 + A1*y2 + b1*x + b2*y + c)"
          "qf x y = 0"
          "qf_1 = (λ x y. x2 + y2 + (b1/A1)*x + (b2/A1)*y + c/A1)"
  shows "qf_1 x y = 0"
proof-
  have "0 = A1*x2 + A1*y2 + b1*x + b2*y + c"
    using assms by auto
  hence "0/A1 = (A1*x2 + A1*y2 + b1*x + b2*y + c)/A1"
    using assms(1) by auto
  also have "... = A1*x2/A1 + A1*y2/A1 + b1*x/A1 + b2*y/A1 + c/A1"
    by (simp add: add_divide_distrib)
  also have "... = x2 + y2 + (b1/A1)*x + (b2/A1)*y + c/A1"
    using assms(1)
    by (simp add:field_simps)
  finally have "0 = x2 + y2 + (b1/A1)*x + (b2/A1)*y + c/A1"
    by simp
  thus ?thesis
    using assms
    by simp
qed

lemma quadratic_quadratic_at_most_2_intersections:
  fixes x y x1 y1 x2 y2 :: complex
  assumes "A1  0" and "A2  0"
  assumes "qf1 = (λ x y. A1*x2 + A1*y2 + b1*x + b2*y + c)" and
          "qf2 = (λ x y. A2*x2 + A2*y2 + B1*x + B2*y + C)" and
          "qf1 x1 y1 = 0" and "qf2 x1 y1 = 0" and
          "qf1 x2 y2 = 0" and "qf2 x2 y2 = 0" and
          "(x1, y1)  (x2, y2)" and
          "qf1 x y = 0" and "qf2 x y = 0"
  assumes "(b2*A2 - B2*A1)2 + (b1*A2 - B1*A1)2  0" and
          "b2*A2  B2*A1  b1*A2  B1*A1"
  shows "(x, y) = (x1, y1)  (x, y) = (x2, y2)"
proof-
  have *: "b2 / A1  B2 / A2  b1 / A1  B1 / A2"
    using assms(1, 2) assms(13)
    by (simp add:field_simps)
  have **: "(b2 / A1 - B2 / A2)2 + (b1 / A1 - B1 / A2)2  0"
    using assms(1, 2) assms(12)
    by (simp add:field_simps)

  let ?qf_1 = "(λ x y. x2 + y2 + (b1/A1)*x + (b2/A1)*y + c/A1)"
  let ?qf_2 = "(λ x y. x2 + y2 + (B1/A2)*x + (B2/A2)*y + C/A2)"

  have "?qf_1 x1 y1 = 0" "?qf_1 x2 y2 = 0" "?qf_1 x y = 0"
       "?qf_2 x1 y1 = 0" "?qf_2 x2 y2 = 0" "?qf_2 x y = 0"
    using assms quadratic_change_coefficients[of A1 qf1 b1 b2 c x2 y2 ?qf_1]
          quadratic_change_coefficients[of A1 qf1 b1 b2 c x1 y1 ?qf_1]
          quadratic_change_coefficients[of A2 qf2 B1 B2 C x1 y1 ?qf_2]
          quadratic_change_coefficients[of A2 qf2 B1 B2 C x2 y2 ?qf_2]
          quadratic_change_coefficients[of A1 qf1 b1 b2 c x y ?qf_1]
          quadratic_change_coefficients[of A2 qf2 B1 B2 C x y ?qf_2]
    by auto

  thus ?thesis
    using quadratic_quadratic_at_most_2_intersections'
              [of "b2 / A1" "B2 / A2" "b1 / A1" "B1 / A2" ?qf_1 "c / A1" ?qf_2 "C / A2" x1 y1 x2 y2 x y]
    using * ** (x1, y1)  (x2, y2)
    by fastforce
qed

end