rw [sub_eq_add_neg, ←add_assoc, add_comm, add_assoc,
    add_assoc, h, add_assoc, add_right_neg, add_zero, add_comm]
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 - reducer + (quotient + reducer) + remainder
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