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