Agda-stdlib: ``+-*-suc`` ?

[mechvel]

Is not m*[1+n] a better name for +-*-suc ?

[MatthewDaggitt]

I'm not sure m*[1+n] is that much clearer than +-*-suc.

Perhaps m*[1+n]≡m+m*n is clearer, but it's much longer...

[gallais]

It is a bit strange though that we have +-suc vs. +-*-suc. I understand that
the second one makes _+_ appear but it's essentially a lemma about _ * (suc _)
just like +-suc is essentially about _ + (suc _).

[MatthewDaggitt]

And to make matters more confusing in Data.Integer.Properties it's called [1+m]*n≡n+m*n.

[gallais]

That would be suc-* though rather than *-suc. ;)