exact sum_eq
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : remainder + Polynomial.Lt p = Polynomial.Lt p + remainder
h₂ : -Polynomial.Lt p + quotient = quotient + -Polynomial.Lt p
⊢ divisible = p + quotient + remainder
no goals