Less algebra

[eponier]

This is an experiment to check on how much we depend on mathcomp.algebra.

It seems that we really depend only on ssralg and ssrnum.

We also depend on:

• ssrint: it seems that we only use the coercion nat >-> Z, I introduced Z.of_nat where appropriate, but we could also declare Z.of_nat as a coercion.
• zmodp: to manipulate ordinals used by nth (one occurrence only)

Note that we still indirectly rely on all algebra because of coqword.

Context: mathcomp 2 slows the compilation down; maybe if we use less of mathcomp, the impact is smaller.

[eponier]

We could also check the dependencies on a per-file basis, but this is probably not worth the work.

[bgregoir]

This looks good, can you also do a PR for coqword ?
Maybe this will allow to do some benchmarks.

[eponier]

Subsumed by #765.