Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Jason Gross <jasongross9@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

Add headers to a few files which were missing them.

- zify_iter_specs is entirely in OCaml
- zify_op has been improved
  * The generation of proof-terms is more direct
  * It does not `rewrite` but instead either performs
    a `pose proof` or a `change`
  * The support for `and`, `or`, `not`, arrow is hardcoded
  * Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)

[micromega] fix stack overflow

Less naive computation of bounds (online elimination of duplicates)

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003