nats: finish proof of no zero divisors for N
nats: prove distributivity, associativity, order-preservation and cancellation law for multiplication