feat(library/standard/nat2): proved x = x div y * y + x mod y
fix(library/standard): fix typo, comment unfinished theorems
fix(library/standard/Makefile,extract_deps): use ENV_VAR LEAN if exists
refactor(library/standard): moved temporary product and some useful theorems to kernel
feat(nat/int/kernel/subtype): Give definition of int based on quotients and make other minor changes

Minor changes in other files: Add some more theorems about tprod in kernel (and some cleanup of long lines); move some code from nat2 to nat; add thm to subtype and changed (Type U) to Type.
chore(library/.gitignore): move to 'library/', add 'make.deps'
chore(library/standard/subtype.lean): change permission
chore(library/Makefile.common): use structured Makefile

 - 'library/Makefile.common' has the common features
 - 'library/standard/Makefile' and 'library/hott/Makefile' just include
   'library/Makefile.common'
 - simplify extract_deps and put it under library/
feat(library/standard/nat2): add a mechanism for a general recursive definition with respect to a nat-valued measure
feat(nat/int/kernel): Prove more theorems about sub in nat; prove that int is a quotient

Add pair extensionality to kernel
Add to nat a lot of theorems with interaction between sub and le
Add to int more properties about the defining relations/functions for int
feat(int): Generalize construction of int

Prove theorem which states that if you pick an element from every equivalence class, then you can form a quotient.
Also define the abstract quotient, which picks an element using the Hilbert operator.
Also allow for quotients of nonreflexive relations.
feat(library/standard/kernel): some useful rules for or
feat(library/standard/nat2): definitions of divides and gcd
fix(library/standard/nat2): improved definitions of div and mod
added facts about div and mod
feat(library/standard/): Develop basic library about integer addition and subtraction, and some minor fixes

Rename the distributivity theorems in nat.lean and nat2.lean.
Separate quotient and int files
Prove most theorems on integer addition, subtraction and negation
fix(library/standard/nat2.lean): redo my changes to nat2.lean

Finished renaming of left/right distributivity
fix(library/standard/kernel.lean): fix typo
feat(library/standard/int): define le, prove some theorems

Prove interaction of le and add, no interaction with sub, neg, etc. yet
feat(library/standard/int): prove more theorems about le, define mul

Prove most interactions of le with other operators. Define multiplication, and prove that it is compatible with the relation on N ## N