Refactor
Add nat examples
Futher clean up Toom-Cook coq proof