∀ {R' : Type u_2} {A : Type u_3} {B : Type u_5} [inst : Ring R'] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {f g : AddMonoidAlgebra R' A},
  AddMonoidAlgebra.supDegree D (f - g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g