Instead of using the nat
type in Coq, it's sometimes (when you have to manipulate big numbers) better to use the Z
type, which is a formalization of integers using a sign magnitude pair representation. The tradeoff is that your proofs might get slightly more complex; nat
is very simple, and so admits simple proof principles.
However, in Coq there's an extensive use of notation to make it simpler to write definitions, theorems, and proofs. Coq has an extremely small kernel (we want this because we want to be able to believe the proof checker is correct, and we can read that) with a lot of notation on top of it. However, as there are different representations of things, and only a few good symbols, our symbols typically clash. To get past this, coq uses interpretation scopes to disambiguate symbols, and resolve them into names (because "+" means add
, plus
, etc...).
You are correct, using Z_scope
is where, +
for plus
within Z
.