have h: remainder + Polynomial.Lt p = Polynomial.Lt p + remainder := 
  add_comm 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
⊢ 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
⊢ divisible = p - Polynomial.Lt p + quotient + (remainder + Polynomial.Lt p)