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