Remove remainder of `Abort`s in test-suite Nia.v
Remove remainder of `Abort`s in test-suite Nia.v

Note that we define a `cleanup` tactic which is essential for speed of
reasoning.  Perhaps this tactic should make it into the code for
`Z.div_mod_to_quot_rem` somewhere?

```coq
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.
```

Matafou/coq,JasonGross/coq,gares/coq,Zimmi48/coq,ejgallego/coq,ejgallego/coq,ejgallego/coq,SkySkimmer/coq,ppedrot/coq,SkySkimmer/coq,gares/coq,gares/coq,Zimmi48/coq,JasonGross/coq,Zimmi48/coq,JasonGross/coq,maximedenes/coq,maximedenes/coq,Matafou/coq,SkySkimmer/coq,gares/coq,gares/coq,maximedenes/coq,silene/coq,coq/coq,ppedrot/coq,silene/coq,maximedenes/coq,ppedrot/coq,Zimmi48/coq,maximedenes/coq,ejgallego/coq,coq/coq,silene/coq,ppedrot/coq,SkySkimmer/coq,JasonGross/coq,coq/coq,ppedrot/coq,Matafou/coq,coq/coq