∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k] (n : ℕ)
  (a : SkewMonoidAlgebra k G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a