The standard library seems to contain various approaches to arithmetic operations on `nat`

.

This includes files mentioned to be “mostly OBSOLETE now”.

Depending on which files/modules are imported, the available properties/lemmas seem to be different.

What is the current recommended way to use arithmetic operations on `nat`

? what should be imported? is there a natural place where one can find (a list of) the available properties? if not, would it be interesting to create such an interface file?

Thanks.

1 Like

For a more consistent and carefully structured version of arithmetic on `nat`

, I recommend `ssrnat.v`

in MathComp’s ssreflect package, (`coq-mathcomp-ssreflect`

on OPAM). See the comments at the top of the file for documentation of the key operations.

The only crux of using this library is that the `lia`

decision procedure cannot be applied directly most of the time. However, this can be solved by using the ppsimpl package (`coq-ppsimpl`

on OPAM).

One example:

```
Require Import Lia.
From PP Require Import Ppsimplmathcomp.
From mathcomp Require Import all_ssreflect.
(*...*)
have Ht: (size trace <= n.+2) by ppsimpl; lia.
```