Implemented wrapping of mixin in bigop.v for files monoid.v and nmodule.v - #1435

- some comments with renaming to be considered in `bigop.v`

- In `nmodule.v` added a structure with just the mixin `hasZero`. This is necessary to avoid an error in `ssralg.v`

- In `nmodule.v` adjusted a comment related to a bug in instantiating commutativity for the key `to_multiplicative` (the whole piece of code seems to be superfluos at this point)

- In `ssralg.v` imported `monoid.v`, so that the mixin of `bigop.v` can be used for the moltiplicative part of ring/algebras

- In `ssralg.v` wrapped the distributivity and annihilative mixins in explicit wrappers. The old mixin `Nmodule_isPzSemiRing` is now a factory.
	(in the process defining extra structures is necessary to avoid the bug exposed in HB#wrapping tests/MinimalWrapBugs/structVS2mixin.v*)

- Applied workaround (denoted by comments) for a bug not allowing to use some factories (involving wrapped mixin) to instantiate structures

NOTE: somehow something is changed in the way the tactic `rewrite` match the goals. This required some minor adjustment to the proof of `exprMn_n`, `prodrN`, `sqrrB1`. Also a type in `exp` needs to be explictly specified (all in `ssralg.v`)

NOTE: `ssralg.v` now crashes after the `Scale` module.

Added comment suggesting a renaming

In c7857f24eaa4149d9021955666b48eb4ef346c69 an HB bug was fixed concerning the declaration of instances using factories involving wrapped arguments.

This commit replace the workarounds for such bug with `HB.instance Definition _ := [factory name].Build ...`

Following the fix in c7857f24eaa4149d9021955666b48eb4ef346c69 we can instantiate without wrapping a key which was wrapped before

I suggest to consider deprecating it since its just a duplicate of `isUMagmaMorphism`

…. The former mixin is now a factory

…round

…for monoid morphisms

… of using `NmoduleMonoid_isPzSemiRing`

… be?

Is it ok to export all the structures this way?

Something seems off with `rewrite`: it search first in the RHS. Similiar problem appear once when  introducing variables

The fail in `numdomain.v` seems to be related to scopes.

First fixes.
See discussion at https://rocq-prover.zulipchat.com/#narrow/channel/237664-math-comp-users/topic/group_scope.20and.20monoid.2Ev/with/526357466

See discussion at https://rocq-prover.zulipchat.com/#narrow/channel/237664-math-comp-users/topic/group_scope.20and.20monoid.2Ev/with/526357466

See discussion at https://rocq-prover.zulipchat.com/#narrow/channel/237664-math-comp-users/topic/group_scope.20and.20monoid.2Ev/with/526357466

`mulrn_char` is never used as a notation in this file and is given as a definition later in the file. Leaving both yelds `Error: Attribute for note specified twice.`

…tive one.

We thus make it local and use an alias in order to still have a global one

…tructure in fingroupmixin and the intended ring structure.

Here, since group is under ring, we have the multiplicative structure there (which is not a group since there are not inverses).

We work around this by juggling aliases. Maybe something like `finzmod` would be needed as a long term fix