Could `abel` be extended to cover `n • x` for arbitrary `n`?

Stream: mathlib4

[Terence Tao]

abel can easily handle identities involving n • x for fixed numerical n, e.g.

example {G:Type} [AddCommGroup G] (x:G) : 2 • x = x + x := by abel -- works

example {G:Type} [AddCommGroup G] (x:G) : (2*3) • x = 2 • (3 • x) := by abel -- works

but would it be technically feasible to also allow it to close some identities involving variable n, e.g.,

example {G:Type} [AddCommGroup G] (x:G) (n:ℕ) : n • x = (n:ℤ) • x := by abel -- fails

example {G:Type} [AddCommGroup G] (x:G) (n:ℤ) : n • (-x) = (-n) • x := by abel -- fails

example {G:Type} [AddCommGroup G] (x:G) (n:ℤ) : n • (-x) = -(n • x) := by abel -- fails

example {G:Type} [AddCommGroup G] (x y:G) (n:ℤ) : n • (x+y) = n • x + n • y := by abel -- fails

example {G:Type} [AddCommGroup G] (x:G) (n m:ℤ) : (n+m) • x = n • x + m • x := by abel -- fails

example {G:Type} [AddCommGroup G] (x:G) (n m:ℤ) : (n*m) • x = n • (m • x) := by abel -- fails

This may be rather non-trivial though (it is asking to have abel take on some of the reduction that ring does), but perhaps there are some cheap normal form reduction tricks that could close some of these use cases.

[Damiano Testa]

module already seems to work in these cases.

[Terence Tao]

Huh, I somehow managed to never encounter this tactic before. For AddCommGroup is it strictly more powerful than abel?

[Damiano Testa]

I don't know if it is strictly more powerful: it tries to write the expression as a smul-combination, but I do not know what other normalisation it does.