feat(nat/kernel): even more theorems for le and lt
Almost done with proving everything for le and lt. Slight modifications to the kernel