theorem Hex.DensePoly.sub_mul_poly {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (a b c : DensePoly S) : (a - b) * c = a * c - b * c

Right distributivity of multiplication over subtraction (Mathlib-free shim: DensePoly carries only Lean.Grind.CommRing).

theorem Hex.DensePoly.degree_getD_sub_lt {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] (a b g : DensePoly S) (hg : 0 < g.degree?.getD 0) (ha : a.degree?.getD 0 < g.degree?.getD 0) (hb : b.degree?.getD 0 < g.degree?.getD 0) : (a - b).degree?.getD 0 < g.degree?.getD 0

The degree?-getD of a difference of two polynomials each of degree below a positive-degree g is again below g.

theorem Hex.DensePoly.divMod_eq_of_reconstruction {S : Type u_1} [Lean.Grind.CommRing S] [DecidableEq S] [Div S] (num g q r : DensePoly S) (hg : 0 < g.degree?.getD 0) (hcancel : ∀ (a : S), a - a / g.leadingCoeff * g.leadingCoeff = Zero.zero) (hexact : ∀ (a : S), a * g.leadingCoeff / g.leadingCoeff = a) (h_top_ne : ∀ (a : S), a ≠ Zero.zero → a * g.leadingCoeff ≠ Zero.zero) (hrec : q * g + r = num) (hrdeg : r.degree?.getD 0 < g.degree?.getD 0) : num.divMod g = (q, r)

Uniqueness of Euclidean division by a positive-degree divisor whose leading coefficient is a two-sided unit (in particular, a monic divisor): a reconstruction with a small remainder is divMod.