Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanup

Also fold it into `Z.div_mod_to_quot_rem`

Note that the test-suite file is a bit slow.  On my machine, it is

```
real    2m32.983s
user    2m32.544s
sys     0m0.492s
```

1 files changed, 2 insertions, 13 deletions

diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index b79a6bde3d..6cb645d9eb 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,20 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
-Ltac cleanup :=
-  repeat match goal with
-         | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
-         | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
-         | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
-         | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
-         | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
-         | _ => progress subst
-         end.
-
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
-    file.  Note that we also add a [cleanup] tactic, which is very
-    important for speed purposes. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; cleanup.
+    file. *)
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
 
 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.