Verify Tez_repr identities
- Rename
positive
predicates tonon_negative
since they are including0
and I need strict positive predicate excluding0
- Added identities of addition, multiplication, subtraction and division in Z at
Environment/Proofs/Pervasives.v
- Added identities of
Tez_repr
addition, multiplication, subtraction and division in Z
Edited by Daniel Hilst