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.

2 files changed, 3 insertions, 2 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.
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 6cb645d9eb..c157173b77 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,7 @@ Open Scope Z_scope.
 
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; subst.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.