rw [h, sub_eq_add_neg, add_assoc,
    add_assoc, add_comm, ←add_assoc,
    ←add_assoc, add_comm, h₂, add_comm, add_assoc, add_comm, 
    add_assoc, add_assoc, add_left_neg, add_zero, add_comm]
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 - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)
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