The standard library seems to contain various approaches to arithmetic operations on
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?
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).
Require Import Lia.
From PP Require Import Ppsimplmathcomp.
From mathcomp Require Import all_ssreflect.
have Ht: (size trace <= n.+2) by ppsimpl; lia.