∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G)
  (x : AddMonoidAlgebra k G), (x.divOf g).support = x.support.preimage (fun x => g + x) ⋯