∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : DecidableEq G] (r : k) (a : G),
  (SkewMonoidAlgebra.single a r * f).support ⊆ Finset.image (fun x => a * x) f.support