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