∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x y : AddMonoidAlgebra k G),
  (x + y).divOf (Multiplicative.toAdd 1) = x.divOf (Multiplicative.toAdd 1) + y.divOf (Multiplicative.toAdd 1)