A gcd bound from the canonical Wronskian inequality

Deduce the finite-extension gcd estimate from the residue-weighted canonical Wronskian bound.

theorem BGS.CorvajaZannier.finiteExtensionGcdBound_of_canonicalWronskianInequality (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) (h k : ℕ) (hn : 0 < h * k + h + k) (chi : ℕ) (hWronskian : Int.ofNat (h * k) * Int.ofNat (finiteExtensionPositiveDegree K L v) - Int.ofNat k * (Int.ofNat (finiteExtensionPositiveDegree K L v) + Int.ofNat (finiteExtensionPositiveDegree K L u)) - Int.ofNat ((h * k + h + k).choose 2) * Int.ofNat chi ≤ Int.ofNat (h * k + h + k) * Int.ofNat (finiteExtensionOutsideHeight K L ((1 - u) / (1 - v)) (propositionTwoExceptionalPlaces K L u v))) : ↑(finiteExtensionGcdWeightedDegree K L (1 - u) (1 - v)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(finiteExtensionPositiveDegree K L v) + ↑k / ↑(h * k + h + k) * ↑(finiteExtensionPositiveDegree K L u) + (↑(h * k + h + k) - 1) / 2 * ↑chi

The exact integer-valued canonical Wronskian inequality, together with the one-minus divisor comparison, implies the numerical bound of Proposition 2 for the exhaustive gcd divisor.