feat(nat): use new kernel
change proofs to be compatible with the kenrel in this library, and prove some more theorems