# 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

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=0∨i=1∨i=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=0∨i=1∨i=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 "P≠0" 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]
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)"
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]
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
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) =
(∑x≤i+1. coeff f x * coeff g (i + 1 - x)) *
(∑x≤i+1. coeff f x * coeff g (i + 1 - x)) -
(∑x≤i+2. coeff f x * coeff g (i + 2 - x)) *
(∑x≤i. 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 "... =
(∑x≤i+1. ∑y≤i+1. coeff f x * coeff g (i + 1 - x) *
coeff f y * coeff g (i + 1 - y)) -
(∑x≤i+2. ∑y≤i. 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 "(∑x≤i + 1. ∑y≤i + 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 "(∑x≤i + 1. ∑y≤i + 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 "(∑x≤i + 2. ∑y≤i. 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 "(∑x≤i + 2. ∑y≤i. 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"
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