I have an issue when trying to work with the type Z: after importing ZArith and writing a theorem that has (a:Z) (b:Z) in its context and then an expression involving (a+b) in the statement, I get the error message " The term "a" has type "Z" while it is expected to have type "nat" ".

More generally, I wanted to ask: is Z the best (or the only) type to work with relative integers? Do the tactics simpl and ring work well with this?

Normally for ZArith you need (a <= b)%Z, but math-comp probably has different approaches than ZArith.

@Paolo Giarrusso Why would I need to assume an inequality if I am adding them?... And even if I subtract them, why should this be an issue in Z? My current problem is about natural numbers, but the reason why I want to work with Z is precisely to avoid structural paradoxes like (2-3)^2=0...

I just typoed the symbol — should have written `(a + b)%Z`

but this uses the stdlib's addition, and I expect that in math-comp you're just not supposed to use that, and you should use the operators that are overloaded via canonical structures.

All right ! Thanks.

In mathcomp, the preferred type of integer is `int`

(from library `mathcomp.algebra.ssrint`

), and you should indeed use the overloaded `+`

in the `ring_scope`

(denoted `%R`

), as in `(m + n)%R`

, since it is canonically a totally ordered integral domain. Unfortunately, `ring`

for this datatype is not yet available officially, although there are have been several attempts that you might get inspiration from (cf math-comp/math-comp#401).

Last updated: Jul 25 2024 at 15:02 UTC