∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {R : Type u_5} [inst_1 : NonUnitalNonAssocSemiring R]
  (f : k →+ R) (g : G → R) (a : G) (b : k), (SkewMonoidAlgebra.liftNC f g) (SkewMonoidAlgebra.single a b) = f b * g a