Theory Normal_Poly

section Normal Polynomials

theory Normal_Poly
  imports "RRI_Misc"
begin

text 
Here we define normal polynomials as defined in
  Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. 
  Springer Berlin Heidelberg, Berlin, Heidelberg (2016).


definition normal_poly :: "('a::{comm_ring_1,ord}) poly  bool" where
"normal_poly p 
  (p  0) 
  ( i. 0  coeff p i) 
  ( i. coeff p i * coeff p (i+2)  (coeff p (i+1))^2) 
  ( i j k. i  j  j  k  0 < coeff p i 
       0 < coeff p k  0 < coeff p j)"

lemma normal_non_zero: "normal_poly p  p  0" 
  using normal_poly_def by blast

lemma normal_coeff_nonneg: "normal_poly p  0  coeff p i" 
  using normal_poly_def by metis

lemma normal_poly_coeff_mult: 
    "normal_poly p  coeff p i * coeff p (i+2)  (coeff p (i+1))^2" 
  using normal_poly_def by blast

lemma normal_poly_pos_interval: 
    "normal_poly p  i  j  j  k  0 < coeff p i  0 < coeff p k 
       0 < coeff p j" 
  using normal_poly_def by blast

lemma normal_polyI:
  assumes "(p  0)"
      and "( i. 0  coeff p i)"
      and "( i. coeff p i * coeff p (i+2)  (coeff p (i+1))^2)"
      and "( i j k. i  j  j  k  0 < coeff p i  0 < coeff p k  0 < coeff p j)"
    shows "normal_poly p"
  using assms by (force simp: normal_poly_def)

lemma linear_normal_iff: 
  fixes x::real 
  shows "normal_poly [:-x, 1:]  x  0"
proof
  assume "normal_poly [:-x, 1:]"
  thus "x  0" using normal_coeff_nonneg[of "[:-x, 1:]" 0] by auto
next
  assume "x  0"
  then have "0  coeff [:- x, 1:] i" for i
    by (cases i) (simp_all add: pCons_one)
  moreover have "0 < coeff [:- x, 1:] j"
    if "i  j" "j  k" "0 < coeff [:- x, 1:] i" 
        "0 < coeff [:- x, 1:] k" for i j k
    apply (cases "k=0  i=0")
    subgoal using that 
      by (smt (z3) bot_nat_0.extremum_uniqueI degree_pCons_eq_if 
          le_antisym le_degree not_less_eq_eq)
    subgoal using that 
      by (smt (z3) One_nat_def degree_pCons_eq_if le_degree less_one
          not_le one_neq_zero pCons_one verit_la_disequality)
    done
  ultimately show "normal_poly [:-x, 1:]"
    unfolding normal_poly_def by auto
qed

lemma quadratic_normal_iff: 
  fixes z::complex 
  shows "normal_poly [:(cmod z)2, -2*Re z, 1:] 
           Re z  0  4*(Re z)^2  (cmod z)^2"
proof
  assume "normal_poly [:(cmod z)2, - 2 * Re z, 1:]"
  hence "-2*Re z  0  (cmod z)^2  0  (-2*Re z)^2  (cmod z)^2"
    using normal_coeff_nonneg[of _ 1] normal_poly_coeff_mult[of _ 0] 
    by fastforce
  thus "Re z  0  4*(Re z)^2  (cmod z)^2"
    by auto
next
  assume asm:"Re z  0  4*(Re z)^2  (cmod z)^2"
  define P where "P=[:(cmod z)2, - 2 * Re z, 1:]"

  have "0  coeff P i" for i 
    unfolding P_def using asm
    apply (cases "i=0i=1i=2")
    by (auto simp:numeral_2_eq_2 coeff_eq_0)
  moreover have "coeff P i * coeff P (i + 2)  (coeff P (i + 1))2" for i
    apply (cases "i=0i=1i=2")
    using asm 
    unfolding P_def by (auto simp:coeff_eq_0)
  moreover have "0 < coeff P j"
    if "0 < coeff P k" "0 < coeff P i" "j  k" "i  j"
    for i j k
    using that unfolding P_def 
    apply (cases "k=0  k=1  k=2")
    subgoal using asm
      by (smt (z3) One_nat_def Suc_1 bot_nat_0.extremum_uniqueI 
          coeff_pCons_0 coeff_pCons_Suc le_Suc_eq 
          zero_less_power2)
    subgoal by (auto simp:coeff_eq_0)
    done
  moreover have "P0" unfolding P_def by auto
  ultimately show "normal_poly P"
    unfolding normal_poly_def by blast
qed

lemma normal_of_no_zero_root: 
  fixes f::"real poly" 
  assumes hzero: "poly f 0  0" and hdeg: "i  degree f" 
    and hnorm: "normal_poly f"
  shows "0 < coeff f i"
proof -
  have "coeff f 0 > 0" using hzero normal_coeff_nonneg[OF hnorm]
    by (metis eq_iff not_le_imp_less poly_0_coeff_0)
  moreover have "coeff f (degree f) > 0" using normal_coeff_nonneg[OF hnorm] normal_non_zero[OF hnorm]
    by (meson dual_order.irrefl eq_iff eq_zero_or_degree_less not_le_imp_less)
  moreover have "0  i" by simp
  ultimately show "0 < coeff f i" using hdeg normal_poly_pos_interval[OF hnorm] by blast
qed

lemma normal_divide_x: 
  fixes f::"real poly" 
  assumes hnorm: "normal_poly (f*[:0,1:])"
  shows "normal_poly f"
proof (rule normal_polyI)
  show "f  0"
    using normal_non_zero[OF hnorm] by auto
next
  fix i
  show "0  coeff f i"
    using normal_coeff_nonneg[OF hnorm, of "Suc i"] by (simp add: coeff_pCons)
next
  fix i
  show "coeff f i * coeff f (i + 2)  (coeff f (i + 1))2"
    using normal_poly_coeff_mult[OF hnorm, of "Suc i"] by (simp add: coeff_pCons)
next
  fix i j k
  show "i  j  j  k  0 < coeff f i  0 < coeff f k  0 < coeff f j"
    using normal_poly_pos_interval[of _ "Suc i" "Suc j" "Suc k", OF hnorm]
    by (simp add: coeff_pCons)
qed

lemma normal_mult_x: 
  fixes f::"real poly" 
  assumes hnorm: "normal_poly f"
  shows "normal_poly (f * [:0, 1:])"
proof (rule normal_polyI)
  show "f * [:0, 1:]  0"
    using normal_non_zero[OF hnorm] by auto
next
  fix i
  show "0  coeff (f * [:0, 1:]) i"
    using normal_coeff_nonneg[OF hnorm, of "i-1"] by (cases i, auto simp: coeff_pCons)
next
  fix i
  show "coeff (f * [:0, 1:]) i * coeff (f * [:0, 1:]) (i + 2)  (coeff (f * [:0, 1:]) (i + 1))2"
    using normal_poly_coeff_mult[OF hnorm, of "i-1"] by (cases i, auto simp: coeff_pCons)
next
  fix i j k
  show "i  j  j  k  0 < coeff (f * [:0, 1:]) i  0 < coeff (f * [:0, 1:]) k  0 < coeff (f * [:0, 1:]) j"
    using normal_poly_pos_interval[of _ "i-1" "j-1" "k-1", OF hnorm]
    apply (cases i, force)
    apply (cases j, force)
    apply (cases k, force)
    by (auto simp: coeff_pCons)
qed

lemma normal_poly_general_coeff_mult: 
  fixes f::"real poly" 
  assumes "normal_poly f" and "h  j"
  shows "coeff f (h+1) * coeff f (j+1)  coeff f h * coeff f (j+2)"
using assms proof (induction j)
  case 0
  then show ?case
    using normal_poly_coeff_mult by (auto simp: power2_eq_square)[1]
next
  case (Suc j)
  then show ?case
  proof (cases "h = Suc j")
    assume "h = Suc j" "normal_poly f"
    thus ?thesis
      using normal_poly_coeff_mult by (auto simp: power2_eq_square)
  next
    assume "(normal_poly f 
       h  j  coeff f h * coeff f (j + 2)  coeff f (h + 1) * coeff f (j + 1))"
      "normal_poly f" and h: "h  Suc j" "h  Suc j"
    hence IH: "coeff f h * coeff f (j + 2)  coeff f (h + 1) * coeff f (j + 1)"
      by linarith
    show ?thesis
    proof (cases "coeff f (Suc j + 1) = 0", cases "coeff f (Suc j + 2) = 0")
      show "coeff f (Suc j + 1) = 0  coeff f (Suc j + 2) = 0 
        coeff f h * coeff f (Suc j + 2)  coeff f (h + 1) * coeff f (Suc j + 1)"
        by (metis assms(1) mult_zero_right normal_coeff_nonneg)
    next
      assume 1: "coeff f (Suc j + 1) = 0" "coeff f (Suc j + 2)  0"
      hence "coeff f (Suc j + 2) > 0" "¬coeff f (Suc j + 1) > 0" 
        using normal_coeff_nonneg[of f "Suc j + 2"] assms(1) by auto
      hence "coeff f h > 0  False"
        using normal_poly_pos_interval[of f h "Suc j + 1" "Suc j + 2"] assms(1) h by force
      hence "coeff f h = 0"
        using normal_coeff_nonneg[OF assms(1)] less_eq_real_def by auto
      thus "coeff f h * coeff f (Suc j + 2)  coeff f (h + 1) * coeff f (Suc j + 1)"
        using 1 by fastforce
    next
      assume 1: "coeff f (Suc j + 1)  0"
      show "coeff f h * coeff f (Suc j + 2)  coeff f (h + 1) * coeff f (Suc j + 1)"
      proof (cases "coeff f (Suc j) = 0")
        assume 2: "coeff f (Suc j) = 0"
        hence "coeff f (Suc j + 1) > 0" "¬coeff f (Suc j) > 0" 
          using normal_coeff_nonneg[of f "Suc j + 1"] assms(1) 1 by auto
        hence "coeff f h > 0  False"
          using normal_poly_pos_interval[of f h "Suc j" "Suc j + 1"] assms(1) h by force
        hence "coeff f h = 0"
          using normal_coeff_nonneg[OF assms(1)] less_eq_real_def by auto
        thus "coeff f h * coeff f (Suc j + 2)  coeff f (h + 1) * coeff f (Suc j + 1)"
          by (simp add: assms(1) normal_coeff_nonneg)
      next
        assume 2: "coeff f (Suc j)  0"
        from normal_poly_coeff_mult[OF assms(1), of "Suc j"] normal_coeff_nonneg[OF assms(1), of "Suc j"]
          normal_coeff_nonneg[OF assms(1), of "Suc (Suc j)"] 1 2 
        have 3: "coeff f (Suc j + 1) / coeff f (Suc j)  coeff f (Suc j + 2) / coeff f (Suc j + 1)"
          by (auto simp: power2_eq_square divide_simps algebra_simps)
        have "(coeff f h * coeff f (j + 2)) * (coeff f (Suc j + 2) / coeff f (Suc j + 1))  (coeff f (h + 1) * coeff f (j + 1)) * (coeff f (Suc j + 1) / coeff f (Suc j))"
          apply (rule mult_mono[OF IH])
          using 3 by (simp_all add: assms(1) normal_coeff_nonneg)
        thus "coeff f h * coeff f (Suc j + 2)  coeff f (h + 1) * coeff f (Suc j + 1)"
          using 1 2 by fastforce
      qed
    qed
  qed
qed

lemma normal_mult: 
  fixes f g::"real poly"
  assumes hf: "normal_poly f" and hg: "normal_poly g"
  defines "df  degree f" and "dg  degree g"
  shows "normal_poly (f*g)"
using df_def hf proof (induction df arbitrary: f)
text We shall first show that without loss of generality we may assume poly f 0 ≠ 0›,
      this is done by induction on the degree, if 0 is a root then we derive the result from f/[:0,1:]›.
  fix f::"real poly" fix i::nat
  assume "0 = degree f" and hf: "normal_poly f"
  then obtain a where "f = [:a:]" using degree_0_iff by auto
  then show "normal_poly (f*g)"
    apply (subst normal_polyI)
    subgoal using normal_non_zero[OF hf] normal_non_zero[OF hg] by auto
    subgoal 
      using normal_coeff_nonneg[of _ 0, OF hf] normal_coeff_nonneg[OF hg] 
      by simp
    subgoal 
      using normal_coeff_nonneg[of _ 0, OF hf] normal_poly_coeff_mult[OF hg] 
      by (auto simp: algebra_simps power2_eq_square mult_left_mono)[1]
    subgoal 
      using normal_non_zero[OF hf] normal_coeff_nonneg[of _ 0, OF hf] normal_poly_pos_interval[OF hg]
      by (simp add: zero_less_mult_iff)
    subgoal by simp
    done
next
  case (Suc df)
  then show ?case
  proof (cases "poly f 0 = 0")
    assume "poly f 0 = 0" and hf:"normal_poly f"
    moreover then obtain f' where hdiv: "f = f'*[:0,1:]"
      by (smt (verit) dvdE mult.commute poly_eq_0_iff_dvd) 
    ultimately have hf': "normal_poly f'" using normal_divide_x by blast
    assume "Suc df = degree f"
    hence "degree f' = df" using hdiv normal_non_zero[OF hf'] by (auto simp: degree_mult_eq)
    moreover assume "f. df = degree f  normal_poly f  normal_poly (f * g)"
    ultimately have "normal_poly (f'*g)" using hf' by blast
    thus "normal_poly (f*g)" using hdiv normal_mult_x by fastforce
  next
    assume hf: "normal_poly f" and hf0: "poly f 0  0"
    define dg where "dg  degree g"
    show "normal_poly (f * g)"
    using dg_def hg proof (induction dg arbitrary: g)
      text Similarly we may assume poly g 0 ≠ 0›.
      fix g::"real poly" fix i::nat
      assume "0 = degree g" and hg: "normal_poly g"
      then obtain a where "g = [:a:]" using degree_0_iff by auto
      then show "normal_poly (f*g)"
        apply (subst normal_polyI)
        subgoal 
          using normal_non_zero[OF hg] normal_non_zero[OF hf] by auto
        subgoal 
          using normal_coeff_nonneg[of _ 0, OF hg] normal_coeff_nonneg[OF hf] 
          by simp
        subgoal 
          using normal_coeff_nonneg[of _ 0, OF hg] normal_poly_coeff_mult[OF hf] 
          by (auto simp: algebra_simps power2_eq_square mult_left_mono)
        subgoal 
          using normal_non_zero[OF hf] normal_coeff_nonneg[of _ 0, OF hg] 
            normal_poly_pos_interval[OF hf]
          by (simp add: zero_less_mult_iff)
        by simp
    next
      case (Suc dg)
      then show ?case
      proof (cases "poly g 0 = 0")
        assume "poly g 0 = 0" and hg:"normal_poly g"
        moreover then obtain g' where hdiv: "g = g'*[:0,1:]"
          by (smt (verit) dvdE mult.commute poly_eq_0_iff_dvd) 
        ultimately have hg': "normal_poly g'" using normal_divide_x by blast
        assume "Suc dg = degree g"
        hence "degree g' = dg" using hdiv normal_non_zero[OF hg'] by (auto simp: degree_mult_eq)
        moreover assume "g. dg = degree g  normal_poly g  normal_poly (f * g)"
        ultimately have "normal_poly (f*g')" using hg' by blast
        thus "normal_poly (f*g)" using hdiv normal_mult_x by fastforce
      next
        text It now remains to show that $(fg)_i \geq 0$. This follows by decomposing $\{(h, j) \in
              \mathbf{Z}^2 | h > j\} = \{(h, j) \in \mathbf{Z}^2 | h \leq j\} \cup \{(h, h - 1) \in 
              \mathbf{Z}^2 | h \in \mathbf{Z}\}$.
              Note in order to avoid working with infinite sums over integers all these sets are
              bounded, which adds some complexity compared to the proof of lemma 2.55 in
              Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry.
              Springer Berlin Heidelberg, Berlin, Heidelberg (2016).
        assume hg0: "poly g 0  0" and hg: "normal_poly g"
        have "f * g  0" using hf hg by (simp add: normal_non_zero Suc.prems)
        moreover have "i. coeff (f*g) i  0"
          apply (subst coeff_mult, rule sum_nonneg, rule mult_nonneg_nonneg)
          using normal_coeff_nonneg[OF hf] normal_coeff_nonneg[OF hg] by auto
        moreover have "
          coeff (f*g) i * coeff (f*g) (i+2)  (coeff (f*g) (i+1))^2" for i
        proof -

          text $(fg)_{i+1}^2 - (fg)_i(fg)_{i+2} = \left(\sum_x f_xg_{i+1-x}\right)^2 - 
                \left(\sum_x f_xg_{i+2-x}\right)\left(\sum_x f_xg_{i-x}\right)$
          have "(coeff (f*g) (i+1))^2 - coeff (f*g) i * coeff (f*g) (i+2) = 
              (xi+1. coeff f x * coeff g (i + 1 - x)) *
              (xi+1. coeff f x * coeff g (i + 1 - x)) -
              (xi+2. coeff f x * coeff g (i + 2 - x)) *
              (xi. coeff f x * coeff g (i - x))"
            by (auto simp: coeff_mult power2_eq_square algebra_simps)
          
          text $\dots = \sum_{x, y} f_xg_{i+1-x}f_yg_{i+1-y} - \sum_{x, y} f_xg_{i+2-x}f_yg_{i-y}$
          also have "... =
              (xi+1. yi+1. coeff f x * coeff g (i + 1 - x) *
                                  coeff f y * coeff g (i + 1 - y)) -
              (xi+2. yi. coeff f x * coeff g (i + 2 - x) *
                                coeff f y * coeff g (i - y))"
            by (subst sum_product, subst sum_product, auto simp: algebra_simps)

          text $\dots = \sum_{h \leq j} f_hg_{i+1-h}f_jg_{i+1-j} + \sum_{h>j} f_hg_{i+1-h}f_jg_{i+1-j}
                       - \sum_{h \leq j} f_hg_{i+2-h}f_jg_{i-j} - \sum_{h>j} f_hg_{i+2-h}f_jg_{i-j}$
          also have "... =
              ((h, j){(h, j). i+1  j  j  h}. 
                coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) +
              ((h, j){(h, j). i+1  h  h > j}. 
                coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) -
             (((h, j){(h, j). i  j  j  h}. 
                coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) +
              ((h, j){(h, j). i + 2  h  h > j  i  j}.
                coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)))"
          proof -
            have "(xi + 1. yi + 1. coeff f x * coeff g (i + 1 - x) * coeff f y * coeff g (i + 1 - y)) =
              ((h, j){(h, j). j  i + 1  h  j}.
                 coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) +
              ((h, j){(h, j). h  i + 1  j < h}.
                 coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))"
            proof (subst sum.union_disjoint[symmetric])
              have H:"{(h, j). j  i + 1  h  j}  {..i+1} × {..i+1}"
                     "{(h, j). h  i + 1  j < h}  {..i+1} × {..i+1}"
                     "finite ({..i+1} × {..i+1})"
                by (fastforce, fastforce, fastforce)
              show "finite {(h, j). j  i + 1  h  j}"
                apply (rule finite_subset) using H by (blast, blast)
              show "finite {(h, j). h  i + 1  j < h}"
                apply (rule finite_subset) using H by (blast, blast)
              show "{(h, j). j  i + 1  h  j}  {(h, j). h  i + 1  j < h} = {}"
                by fastforce
              show "(xi + 1. yi + 1. coeff f x * coeff g (i + 1 - x) * coeff f y * coeff g (i + 1 - y)) =
                  ((h, j){(h, j). j  i + 1  h  j}  {(h, j). h  i + 1  j < h}.
                    coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))"
                apply (subst sum.cartesian_product, rule sum.cong)
                apply force by blast
            qed
            moreover have "(xi + 2. yi. coeff f x * coeff g (i + 2 - x) * coeff f y * coeff g (i - y)) =
               ((h, j){(h, j). j  i  h  j}.
                  coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) +
               ((h, j){(h, j). i + 2  h  h > j  i  j}.
                  coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))"
            proof (subst sum.union_disjoint[symmetric])
              have H:"{(h, j). j  i  h  j}  {..i+2} × {..i}"
                     "{(h, j). i + 2  h  h > j  i  j}  {..i+2} × {..i}"
                     "finite ({..i+2} × {..i})"
                by (fastforce, fastforce, fastforce)
              show "finite {(h, j). j  i  h  j}"
                apply (rule finite_subset) using H by (blast, blast)
              show "finite {(h, j). i + 2  h  h > j  i  j}"
                apply (rule finite_subset) using H by (blast, blast)
              show "{(h, j). j  i  h  j}  {(h, j). i + 2  h  h > j  i  j} = {}"
                by fastforce
              show "(xi + 2. yi. coeff f x * coeff g (i + 2 - x) * coeff f y * coeff g (i - y)) =
                  ((h, j){(h, j). j  i  h  j}  {(h, j). i + 2  h  h > j  i  j}.
                     coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))"
                apply (subst sum.cartesian_product, rule sum.cong)
                apply force by blast
            qed
            ultimately show ?thesis by presburger
          qed

          text $\dots = \sum_{h \leq j} f_hg_{i+1-h}f_jg_{i+1-j} + \sum_{h \leq j} f_{j+1}g_{i-j}f_{h-2}g_{i+2-h} 
                       + \sum_h f_hg_{i+1-h}f_{h-1}g_{i+2-h} - \sum_{h \leq j} f_hg_{i+2-h}f_jg_{i-j}
                       - \sum_{h \leq j} f_{j+1}g_{i+1-j}f_{h-2}g_{i+1-h} - \sum_h f_hg_{i+2-h}f_{h-1}g_{i+1-h}$
          also have "... =
              ((h, j){(h, j). j  i + 1  h  j}.
                 coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) +
              ((h, j){(h, j). j  i  h  j  0 < h}.
                 coeff f (j+1) * coeff g (i - j) * coeff f (h-1) * coeff g (i + 2 - h)) +
              (h{1..i+1}.
                 coeff f h * coeff g (i + 1 - h) * coeff f (h-1) * coeff g (i + 2 - h)) -
              (((h, j){(h, j). j  i  h  j}.
                  coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) +
               ((h, j){(h, j). j  i + 1  h  j  0 < h}.
                  coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)) +
               (h{1..i+1}.
                  coeff f h * coeff g (i + 2 - h) * coeff f (h-1) * coeff g (i + 1 - h)))"
          proof -
            have "((h, j){(h, j). h  i + 1  j < h}.
                   coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j)) = 
                  ((h, j){(h, j). j  i  h  j  0 < h}.
                   coeff f (j + 1) * coeff g (i - j) * coeff f (h - 1) * coeff g (i + 2 - h)) +
                  (h = 1..i + 1. coeff f h * coeff g (i + 1 - h) * coeff f (h - 1) * coeff g (i + 2 - h))"
            proof -
              have 1: "((h, j){(h, j). j  i  h  j  0 < h}.
                     coeff f (j + 1) * coeff g (i - j) * coeff f (h - 1) * coeff g (i + 2 - h)) =
                    ((h, j){(h, j). h  i + 1  j < h  h  j + 1}.
                     coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))"
              proof (rule sum.reindex_cong)
                show "{(h, j). j  i  h  j  0 < h} = (λ(h, j). (j+1, h-1)) ` {(h, j). h  i + 1  j < h  h  j + 1}"
                proof
                  show "(λ(h, j). (j + 1, h - 1)) ` {(h, j). h  i + 1  j < h  h  j + 1}  {(h, j). j  i  h  j  0 < h}"
                    by fastforce
                  show "{(h, j). j  i  h  j  0 < h}  (λ(h, j). (j + 1, h - 1)) ` {(h, j). h  i + 1  j < h  h  j + 1}"
                  proof
                    fix x
                    assume "x  {(h, j). j  i  h  j  0 < h}"
                    then obtain h j where "x = (h, j)" "j  i" "h  j" "0 < h" by blast
                    hence "j + 1  i + 1  h - 1 < j + 1  j + 1  h - 1 + 1  x = ((h - 1) + 1, (j + 1) - 1)"
                      by auto
                    thus "x  (λ(h, j). (j + 1, h - 1)) ` {(h, j). h  i + 1  j < h  h  j + 1}"
                      by (auto simp: image_iff)
                  qed
                qed
                show "inj_on (λ(h, j). (j + 1, h - 1)) {(h, j). h  i + 1  j < h  h  j + 1}"
                proof
                  fix x y::"nat×nat"
                  assume "x  {(h, j). h  i + 1  j < h  h  j + 1}" "y  {(h, j). h  i + 1  j < h  h  j + 1}"
                  thus "(case x of (h, j)  (j + 1, h - 1)) = (case y of (h, j)  (j + 1, h - 1))  x = y"
                    by auto
                qed
                show "x. x  {(h, j). h  i + 1  j < h  h  j + 1} 
                 (case case x of (h, j)  (j + 1, h - 1) of
                  (h, j)  coeff f (j + 1) * coeff g (i - j) * coeff f (h - 1) * coeff g (i + 2 - h)) =
                 (case x of (h, j)  coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))"
                  by fastforce
              qed
              have 2: "(h = 1..i + 1. coeff f h * coeff g (i + 1 - h) * coeff f (h - 1) * coeff g (i + 2 - h)) =
                    ((h, j){(h, j). h  i + 1  j < h  h = j + 1}.
                     coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))"
              proof (rule sum.reindex_cong)
                show "{1..i + 1} = fst ` {(h, j). h  i + 1  j < h  h = j + 1}"
                proof
                  show "{1..i + 1}  fst ` {(h, j). h  i + 1  j < h  h = j + 1}"
                  proof
                    fix x
                    assume "x  {1..i + 1}"
                    hence "x  i + 1  x - 1 < x  x = x - 1 + 1  x = fst (x, x-1)"
                      by auto
                    thus "x  fst ` {(h, j). h  i + 1  j < h  h = j + 1}"
                      by blast
                  qed
                  show "fst ` {(h, j). h  i + 1  j < h  h = j + 1}  {1..i + 1}"
                    by force
                qed
                show "inj_on fst {(h, j). h  i + 1  j < h  h = j + 1}"
                proof
                  fix x y
                  assume "x  {(h, j). h  i + 1  j < h  h = j + 1}"
                         "y  {(h, j). h  i + 1  j < h  h = j + 1}"
                  hence "x = (fst x, fst x - 1)" "y = (fst y, fst y - 1)" "fst x > 0" "fst y > 0"
                    by auto
                  thus "fst x = fst y  x = y" by presburger
                qed
                show "x. x  {(h, j). h  i + 1  j < h  h = j + 1} 
                   coeff f (fst x) * coeff g (i + 1 - fst x) * coeff f (fst x - 1) * coeff g (i + 2 - fst x) =
                   (case x of (h, j)  coeff f h * coeff g (i + 1 - h) * coeff f j * coeff g (i + 1 - j))"
                  by fastforce
              qed
              have H: "{(h, j). h  i + 1  j < h  h  j + 1}  {0..i+1}×{0..i+1}"
                      "{(h, j). h  i + 1  j < h  h = j + 1}  {0..i+1}×{0..i+1}"
                      "finite ({0..i+1}×{0..i+1})"
                by (fastforce, fastforce, fastforce)
              have "finite {(h, j). h  i + 1  j < h  h  j + 1}"
                   "finite {(h, j). h  i + 1  j < h  h = j + 1}"
                apply (rule finite_subset) using H apply (simp, simp)
                apply (rule finite_subset) using H apply (simp, simp)
                done
              thus ?thesis 
                apply (subst 1, subst 2, subst sum.union_disjoint[symmetric])
                   apply auto[3]
                apply (rule sum.cong)
                by auto
            qed
            moreover have "((h, j){(h, j). h  i + 2  j < h  j  i}.
                  coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j)) = 
               ((h, j){(h, j). j  i + 1  h  j  0 < h}.
                  coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) +
               (h = 1..i + 1. coeff f h * coeff g (i + 2 - h) * coeff f (h - 1) * coeff g (i + 1 - h))"
            proof -
              have 1: "((h, j){(h, j). j  i + 1  h  j  0 < h}.
                     coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) =
                    ((h, j){(h, j). h  i + 2  j < h  j  i  h  j + 1}.
                     coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))"
              proof (rule sum.reindex_cong)
                show "{(h, j). j  i + 1  h  j  0 < h} = (λ(h, j). (j+1, h-1)) ` {(h, j). h  i + 2  j < h  j  i  h  j + 1}"
                proof
                  show "(λ(h, j). (j + 1, h - 1)) ` {(h, j). h  i + 2  j < h  j  i  h  j + 1}  {(h, j). j  i + 1  h  j  0 < h}"
                    by fastforce
                  show "{(h, j). j  i + 1  h  j  0 < h}  (λ(h, j). (j + 1, h - 1)) ` {(h, j). h  i + 2  j < h  j  i  h  j + 1}"
                  proof
                    fix x
                    assume "x  {(h, j). j  i + 1  h  j  0 < h}"
                    then obtain h j where "x = (h, j)" "j  i + 1" "h  j" "0 < h" by blast
                    hence "j + 1  i + 2  h - 1 < j + 1  h - 1  i  j + 1  h - 1 + 1  x = ((h - 1) + 1, (j + 1) - 1)"
                      by auto
                    thus "x  (λ(h, j). (j + 1, h - 1)) ` {(h, j). h  i + 2  j < h  j  i  h  j + 1}"
                      by (auto simp: image_iff)
                  qed
                qed
                show "inj_on (λ(h, j). (j + 1, h - 1)) {(h, j). h  i + 2  j < h  j  i  h  j + 1}"
                proof
                  fix x y::"nat×nat"
                  assume "x  {(h, j). h  i + 2  j < h  j  i  h  j + 1}" "y  {(h, j). h  i + 2  j < h  j  i  h  j + 1}"
                  thus "(case x of (h, j)  (j + 1, h - 1)) = (case y of (h, j)  (j + 1, h - 1))  x = y"
                    by auto
                qed
                show "x. x  {(h, j). h  i + 2  j < h  j  i  h  j + 1} 
                   (case case x of (h, j)  (j + 1, h - 1) of
                    (h, j)  coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) =
                   (case x of (h, j)  coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))"
                  by fastforce
              qed
              have 2: "(h = 1..i + 1. coeff f h * coeff g (i + 2 - h) * coeff f (h - 1) * coeff g (i + 1 - h)) =
                    ((h, j){(h, j). h  i + 2  j < h  j  i  h = j + 1}.
                     coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))"
              proof (rule sum.reindex_cong)
                show "{1..i + 1} = fst ` {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                proof
                  show "{1..i + 1}  fst ` {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                  proof
                    fix x
                    assume "x  {1..i + 1}"
                    hence "x  i + 2  x - 1 < x  x - 1  i  x = x - 1 + 1  x = fst (x, x-1)"
                      by auto
                    thus "x  fst ` {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                      by blast
                  qed
                  show "fst ` {(h, j). h  i + 2  j < h  j  i  h = j + 1}  {1..i + 1}"
                    by force
                qed
                show "inj_on fst {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                proof
                  fix x y
                  assume "x  {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                         "y  {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                  hence "x = (fst x, fst x - 1)" "y = (fst y, fst y - 1)" "fst x > 0" "fst y > 0"
                    by auto
                  thus "fst x = fst y  x = y" by presburger
                qed
                show "x. x  {(h, j). h  i + 2  j < h  j  i  h = j + 1} 
                   coeff f (fst x) * coeff g (i + 2 - fst x) * coeff f (fst x - 1) * coeff g (i + 1 - fst x) =
                   (case x of (h, j)  coeff f h * coeff g (i + 2 - h) * coeff f j * coeff g (i - j))"
                  by fastforce
              qed
              have H: "{(h, j). h  i + 2  j < h  j  i  h  j + 1}  {0..i+2}×{0..i}"
                      "{(h, j). h  i + 2  j < h  j  i  h = j + 1}  {0..i+2}×{0..i}"
                      "finite ({0..i+2}×{0..i})"
                by (fastforce, fastforce, fastforce)
              have "finite {(h, j). h  i + 2  j < h  j  i  h  j + 1}"
                   "finite {(h, j). h  i + 2  j < h  j  i  h = j + 1}"
                apply (rule finite_subset) using H apply (simp, simp)
                apply (rule finite_subset) using H apply (simp, simp)
                done
              thus ?thesis 
                apply (subst 1, subst 2, subst sum.union_disjoint[symmetric])
                   apply auto[3]
                apply (rule sum.cong)
                by auto
            qed
            ultimately show ?thesis
              by algebra
          qed

          text $\dots = \sum_{h \leq j} f_hf_j\left(g_{i+1-h}g_{i+1-j} - g_{i+2-h}g_{i-j}\right) + 
                         \sum_{h \leq j} f_{j+1}f_{h-1}\left(g_{i-j}g_{i+2-h} - g_{i+1-j}f_jg_{i+1-h}\right)$

                Note we have to also consider the edge cases caused by making these sums finite.
          also have "... =
              ((h, j){(h, j). j = i + 1  h  j}.
                 coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) +
              ((h, j){(h, j). j  i  h  j}.
                 coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) +
              ((h, j){(h, j). j  i  h  j  0 < h}.
                 coeff f (j+1) * coeff f (h-1) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h))) -
              (((h, j){(h, j). j = i + 1  h  j  0 < h}.
                  coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)))" (is "?L = ?R")
          proof -
            have "?R = 
              ((h, j){(h, j). j = i + 1  h  j}.
                 coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) +
              (((h, j){(h, j). j  i  h  j}.
                 coeff f h * coeff f j * coeff g (i + 1 - h) * coeff g (i + 1 - j)) -
              ((h, j){(h, j). j  i  h  j}.
                 coeff f h * coeff f j * coeff g (i + 2 - h) * coeff g (i - j))) +
              (((h, j){(h, j). j  i  h  j  0 < h}.
                 coeff f (j+1) * coeff f (h-1) * coeff g (i - j) * coeff g (i + 2 - h)) - 
              ((h, j){(h, j). j  i  h  j  0 < h}.
                 coeff f (j+1) * coeff f (h-1) * coeff g (i + 1 - j) * coeff g (i + 1 - h))) -
              (((h, j){(h, j). j = i + 1  h  j  0 < h}.
                  coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)))"
              apply (subst sum_subtractf[symmetric], subst sum_subtractf[symmetric])
              by (auto simp: algebra_simps split_beta)
            also have "... =
                (((h, j){(h, j). j = i + 1  h  j}.
                   coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) +
                ((h, j){(h, j). j  i  h  j}.
                   coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j)))) -
                 ((h, j){(h, j). j  i  h  j}.
                    coeff f h * coeff f j * coeff g (i + 2 - h) * coeff g (i - j)) +
                ((h, j){(h, j). j  i  h  j  0 < h}.
                    coeff f (j + 1) * coeff f (h - 1) * coeff g (i - j) * coeff g (i + 2 - h)) -
                (((h, j){(h, j). j  i  h  j  0 < h}.
                   coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) +
                ((h, j){(h, j). j = i + 1  h  j  0 < h}.
                   coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)))"
              by (auto simp: algebra_simps)
            also have "... = ?L"
            proof -
              have "((h, j){(h, j). j = i + 1  h  j}.
                       coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) +
                    ((h, j){(h, j). j  i  h  j}.
                       coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) =
                    ((h, j){(h, j). j  i + 1  h  j}.
                       coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j)))"
              proof (subst sum.union_disjoint[symmetric])
                have "{(h, j). j = i + 1  h  j}  {..i + 1} × {..i + 1}"
                     "{(h, j). j  i  h  j}  {..i + 1} × {..i + 1}"
                  by (fastforce, fastforce)
                thus "finite {(h, j). j = i + 1  h  j}" "finite {(h, j). j  i  h  j}"
                  by (auto simp: finite_subset)
                show "{(h, j). j = i + 1  h  j}  {(h, j). j  i  h  j} = {}"
                  by fastforce
              qed (rule sum.cong, auto)
              moreover have "((h, j){(h, j). j  i  h  j  0 < h}.
                    coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) +
                 ((h, j){(h, j). j = i + 1  h  j  0 < h}.
                    coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) =
                 ((h, j){(h, j). j  i + 1  h  j  0 < h}.
                    coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h))"
              proof (subst sum.union_disjoint[symmetric])
                have "{(h, j). j  i  h  j  0 < h}  {..i + 1} × {..i + 1}"
                     "{(h, j). j = i + 1  h  j  0 < h}  {..i + 1} × {..i + 1}"
                  by (fastforce, fastforce)
                thus "finite {(h, j). j  i  h  j  0 < h}" "finite {(h, j). j = i + 1  h  j  0 < h}"
                  by (auto simp: finite_subset)
                show "{(h, j). j  i  h  j  0 < h}  {(h, j). j = i + 1  h  j  0 < h} = {}"
                  by fastforce
              qed (rule sum.cong, auto)
              ultimately show ?thesis 
                by (auto simp: algebra_simps)
            qed
            finally show ?thesis by presburger
          qed

          text $\dots = \sum_{h \leq j} \left(f_hf_j - f_{j+1}f_{h-1}\right)
                                         \left(g_{i+1-h}g_{i+1-j} - g_{i+2-h}g_{i-j}\right)$
          also have "... = 
              ((h, j){(h, j). j  i  h  j  0 < h}.
                 -(coeff f h * coeff f j - coeff f (j+1) * coeff f (h-1)) * (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h))) +
              ((h, j){(h, j). j  i  h  j  h = 0}.
                 coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) +
              ((h, j){(h, j). j = i + 1  h  j}.
                 coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) -
              (((h, j){(h, j). j = i + 1  h  j  0 < h}.
                  coeff f (j+1) * coeff g (i + 1 - j) * coeff f (h-1) * coeff g (i + 1 - h)))" (is "?L = ?R")
          proof -
            have "((h, j){(h, j). j  i  h  j}.
               coeff f h * coeff f j *
               (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) =
             ((h, j){(h, j). j  i  h  j  0 < h}.
               coeff f h * coeff f j *
               (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) +
             ((h, j){(h, j). j  i  h  j  0 = h}.
               coeff f h * coeff f j *
               (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j)))"
            proof (subst sum.union_disjoint[symmetric])
              have "{(h, j). j  i  h  j  0 < h}  {..i}×{..i}" "{(h, j). j  i  h  j  0 = h}  {..i}×{..i}"
                by (force, force)
              thus "finite {(h, j). j  i  h  j  0 < h}" "finite {(h, j). j  i  h  j  0 = h}"
                by (auto simp: finite_subset)
              show "{(h, j). j  i  h  j  0 < h}  {(h, j). j  i  h  j  0 = h} = {}"
                by fast
            qed (rule sum.cong, auto)
            
            moreover have "((h, j){(h, j). j  i  h  j  0 < h}.
               (-coeff f h * coeff f j + coeff f (j + 1) * coeff f (h - 1)) *
               (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h))) =
                ((h, j){(h, j). j  i  h  j  0 < h}.
                   coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j))) +
                ((h, j){(h, j). j  i  h  j  0 < h}.
                   coeff f (j + 1) * coeff f (h - 1) *
                   (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)))"
              by (subst sum.distrib[symmetric], rule sum.cong, fast, auto simp: algebra_simps)

            ultimately show ?thesis
              by (auto simp: algebra_simps)
          qed

          text $\dots \geq 0$ by normal_poly_general_coeff_mult›
          also have "...  0"
          proof -
            have "0  ((h, j){(h, j). j  i  h  j  0 < h}.
                        - (coeff f h * coeff f j - coeff f (j + 1) * coeff f (h - 1)) *
                        (coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)))"
            proof (rule sum_nonneg)
              fix x assume "x  {(h, j). j  i  h  j  0 < h}"
              then obtain h j where H: "x = (h, j)" "j  i" "h  j" "0 < h" by fast
              hence "h - 1  j - 1" by force
              hence 1: "coeff f h * coeff f j - coeff f (j + 1) * coeff f (h - 1)  0"
                using normal_poly_general_coeff_mult[OF hf, of "h-1" "j-1"] H
                by (auto simp: algebra_simps)
              from H have "i - j  i - h" by force
              hence 2: "coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)  0"
                using normal_poly_general_coeff_mult[OF hg, of "i - j" "i - h"] H
                by (smt (verit, del_insts) Nat.add_diff_assoc2 le_trans)
              show "0  (case x of
               (h, j) 
                 - (coeff f h * coeff f j - coeff f (j + 1) * coeff f (h - 1)) *
                 (coeff g (i - j) * coeff g (i + 2 - h) -
                  coeff g (i + 1 - j) * coeff g (i + 1 - h)))"
                apply (subst H(1), subst split, rule mult_nonpos_nonpos, subst neg_le_0_iff_le)
                subgoal using 1 by blast
                subgoal using 2 by blast
                done
            qed
            moreover have "0  ((h, j){(h, j). j  i  h  j  h = 0}.
                        coeff f h * coeff f j *
                        (coeff g (i + 1 - h) * coeff g (i + 1 - j) - coeff g (i + 2 - h) * coeff g (i - j)))"
            proof (rule sum_nonneg)
              fix x assume "x  {(h, j). j  i  h  j  h = 0}"
              then obtain h j where H: "x = (h, j)" "j  i" "h  j" "h = 0" by fast
              have 1: "coeff f h * coeff f j  0"
                by (simp add: hf normal_coeff_nonneg)
              from H have "i - j  i - h" by force
              hence 2: "coeff g (i - j) * coeff g (i + 2 - h) - coeff g (i + 1 - j) * coeff g (i + 1 - h)  0"
                using normal_poly_general_coeff_mult[OF hg, of "i - j" "i - h"] H
                by (smt (verit, del_insts) Nat.add_diff_assoc2 le_trans)
              show "0  (case x of
               (h, j) 
                 coeff f h * coeff f j *
                 (coeff g (i + 1 - h) * coeff g (i + 1 - j) -
                  coeff g (i + 2 - h) * coeff g (i - j)))"
                apply (subst H(1), subst split, rule mult_nonneg_nonneg)
                subgoal using 1 by blast
                subgoal using 2 by argo
                done
            qed
            moreover have "0  ((h, j){(h, j). j = i + 1  h  j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) -
                 ((h, j){(h, j). j = i + 1  h  j  0 < h}.
                    coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h))"
            proof -
              have "((h, j){(h, j). j = i + 1  h  j}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) -
                 ((h, j){(h, j). j = i + 1  h  j  0 < h}.
                    coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h)) = 
                 ((h, j){(h, j). j = i + 1  h  j  h = 0}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) +
                 ((h, j){(h, j). j = i + 1  h  j  0 < h}. coeff f h * coeff f j * (coeff g (i + 1 - h) * coeff g (i + 1 - j))) -
                 ((h, j){(h, j). j = i + 1  h  j  0 < h}.
                    coeff f (j + 1) * coeff g (i + 1 - j) * coeff f (h - 1) * coeff g (i + 1 - h))"
              proof (subst sum.union_disjoint[symmetric])
                have "{(h, j). j = i + 1  h  j  h = 0} = {(0, i + 1)}"
                     "{(h, j). j = i + 1  h  j