feat(nat): more theorems for le and lt
feat(nat/kernel): even more theorems for le and lt
Almost done with proving everything for le and lt. Slight modifications to the kernel
feat(nat): prove all(?) theorems for le and lt
Prove all simple theorems involving only add, mul, le, lt
Nothing involving pred, though
feat(nat): add minus, prove theorems about it
minus is needed to define addition for integers
feat(nat) remove redundant comment
append and head