Add subst to the end of nia in the test-suite

This speeds up the file from 2m32s to

```
real    0m41.851s
user    0m41.512s
sys     0m0.376s
```

Also note the `subst` trick in the doc.

1 files changed, 2 insertions, 1 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 2ace8a59e1..5f199d28f5 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -251,7 +251,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
 .. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by pre-processing the goal with
-  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.
+  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.  Note that additionally
+  running ``subst`` can speed up things up, sometimees by almost 4x in practice.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.