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