[Agda] adding StrictTotalOrder for Integer

[Sergei Meshveliani]

People,

the archive
http://www.botik.ru/pub/local/Mechveliani/agdaNotes/natIntExtProposal.zip

contains a  proposal for addition to the Agda Standard library.

It has been type-checked under  Agda-2.4.0, Standard library 0.8.

This is a conservative addition for the modules 
                       Nat, Nat.Properties, Integer, Integer.Properties.

The items proposed to add are represented by the modules  
                                                 Nat1, Integer1.

Integer1  implements  StrictTotalOrder  for Integer
          -- which, I expect, is needed for standard.

There are also some other items which are not needed for  
Integer1.strictTotalOrder,
which I use, and which the developers could consider for adding.

If asked, I could filter there only the items needed for 
Integer1.strictTotalOrder.

Possible improvements in the proofs are welcome.


About the Git repository
------------------------
I have failed to upload the code on Git for Standard library.
I can create an `issue', to write a comment. 
And I thought that to upload a code one needs to create a 
`pull request' 
(right?). 
Then, after clicking at   New Pull Request
it shows a certain picture with a rolling disc in the middle, and 
all the buttons seem to do something irrelevant, I do not find, how to
upload an archive.

So, I provide a link here.

Regards,

------
Sergei